MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lmodvsdir Structured version   Visualization version   GIF version

Theorem lmodvsdir 19110
Description: Distributive law for scalar product (right-distributivity). (ax-hvdistr1 28196 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
Hypotheses
Ref Expression
lmodvsdir.v 𝑉 = (Base‘𝑊)
lmodvsdir.a + = (+g𝑊)
lmodvsdir.f 𝐹 = (Scalar‘𝑊)
lmodvsdir.s · = ( ·𝑠𝑊)
lmodvsdir.k 𝐾 = (Base‘𝐹)
lmodvsdir.p = (+g𝐹)
Assertion
Ref Expression
lmodvsdir ((𝑊 ∈ LMod ∧ (𝑄𝐾𝑅𝐾𝑋𝑉)) → ((𝑄 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋)))

Proof of Theorem lmodvsdir
StepHypRef Expression
1 lmodvsdir.v . . . . . . . 8 𝑉 = (Base‘𝑊)
2 lmodvsdir.a . . . . . . . 8 + = (+g𝑊)
3 lmodvsdir.s . . . . . . . 8 · = ( ·𝑠𝑊)
4 lmodvsdir.f . . . . . . . 8 𝐹 = (Scalar‘𝑊)
5 lmodvsdir.k . . . . . . . 8 𝐾 = (Base‘𝐹)
6 lmodvsdir.p . . . . . . . 8 = (+g𝐹)
7 eqid 2761 . . . . . . . 8 (.r𝐹) = (.r𝐹)
8 eqid 2761 . . . . . . . 8 (1r𝐹) = (1r𝐹)
91, 2, 3, 4, 5, 6, 7, 8lmodlema 19091 . . . . . . 7 ((𝑊 ∈ LMod ∧ (𝑄𝐾𝑅𝐾) ∧ (𝑋𝑉𝑋𝑉)) → (((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋 + 𝑋)) = ((𝑅 · 𝑋) + (𝑅 · 𝑋)) ∧ ((𝑄 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋))) ∧ (((𝑄(.r𝐹)𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋)) ∧ ((1r𝐹) · 𝑋) = 𝑋)))
109simpld 477 . . . . . 6 ((𝑊 ∈ LMod ∧ (𝑄𝐾𝑅𝐾) ∧ (𝑋𝑉𝑋𝑉)) → ((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋 + 𝑋)) = ((𝑅 · 𝑋) + (𝑅 · 𝑋)) ∧ ((𝑄 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋))))
1110simp3d 1139 . . . . 5 ((𝑊 ∈ LMod ∧ (𝑄𝐾𝑅𝐾) ∧ (𝑋𝑉𝑋𝑉)) → ((𝑄 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋)))
12113expa 1112 . . . 4 (((𝑊 ∈ LMod ∧ (𝑄𝐾𝑅𝐾)) ∧ (𝑋𝑉𝑋𝑉)) → ((𝑄 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋)))
1312anabsan2 898 . . 3 (((𝑊 ∈ LMod ∧ (𝑄𝐾𝑅𝐾)) ∧ 𝑋𝑉) → ((𝑄 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋)))
1413exp42 640 . 2 (𝑊 ∈ LMod → (𝑄𝐾 → (𝑅𝐾 → (𝑋𝑉 → ((𝑄 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋))))))
15143imp2 1443 1 ((𝑊 ∈ LMod ∧ (𝑄𝐾𝑅𝐾𝑋𝑉)) → ((𝑄 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072   = wceq 1632  wcel 2140  cfv 6050  (class class class)co 6815  Basecbs 16080  +gcplusg 16164  .rcmulr 16165  Scalarcsca 16167   ·𝑠 cvsca 16168  1rcur 18722  LModclmod 19086
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-nul 4942
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3343  df-sbc 3578  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-br 4806  df-iota 6013  df-fv 6058  df-ov 6818  df-lmod 19088
This theorem is referenced by:  lmod0vs  19119  lmodvsmmulgdi  19121  lmodvneg1  19129  lmodcom  19132  lmodsubdir  19144  islss3  19182  lss1d  19186  prdslmodd  19192  lspsolvlem  19365  asclghm  19561  frlmup1  20360  scmataddcl  20545  scmatghm  20562  pm2mpghm  20844  clmvsdir  23112  cvsi  23151  lshpkrlem4  34922  baerlem3lem1  37517  baerlem5blem1  37519  hgmapadd  37707  mendlmod  38284  lmodvsmdi  42692  lincsum  42747  ldepsprlem  42790
  Copyright terms: Public domain W3C validator