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

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

Proof of Theorem lmodvsdi
StepHypRef Expression
1 lmodvsdi.v . . . . . . . . 9 𝑉 = (Base‘𝑊)
2 lmodvsdi.a . . . . . . . . 9 + = (+g𝑊)
3 lmodvsdi.s . . . . . . . . 9 · = ( ·𝑠𝑊)
4 lmodvsdi.f . . . . . . . . 9 𝐹 = (Scalar‘𝑊)
5 lmodvsdi.k . . . . . . . . 9 𝐾 = (Base‘𝐹)
6 eqid 2728 . . . . . . . . 9 (+g𝐹) = (+g𝐹)
7 eqid 2728 . . . . . . . . 9 (.r𝐹) = (.r𝐹)
8 eqid 2728 . . . . . . . . 9 (1r𝐹) = (1r𝐹)
91, 2, 3, 4, 5, 6, 7, 8lmodlema 20747 . . . . . . . 8 ((𝑊 ∈ LMod ∧ (𝑅𝐾𝑅𝐾) ∧ (𝑌𝑉𝑋𝑉)) → (((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋 + 𝑌)) = ((𝑅 · 𝑋) + (𝑅 · 𝑌)) ∧ ((𝑅(+g𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋) + (𝑅 · 𝑋))) ∧ (((𝑅(.r𝐹)𝑅) · 𝑋) = (𝑅 · (𝑅 · 𝑋)) ∧ ((1r𝐹) · 𝑋) = 𝑋)))
109simpld 494 . . . . . . 7 ((𝑊 ∈ LMod ∧ (𝑅𝐾𝑅𝐾) ∧ (𝑌𝑉𝑋𝑉)) → ((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋 + 𝑌)) = ((𝑅 · 𝑋) + (𝑅 · 𝑌)) ∧ ((𝑅(+g𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋) + (𝑅 · 𝑋))))
1110simp2d 1141 . . . . . 6 ((𝑊 ∈ LMod ∧ (𝑅𝐾𝑅𝐾) ∧ (𝑌𝑉𝑋𝑉)) → (𝑅 · (𝑋 + 𝑌)) = ((𝑅 · 𝑋) + (𝑅 · 𝑌)))
12113expia 1119 . . . . 5 ((𝑊 ∈ LMod ∧ (𝑅𝐾𝑅𝐾)) → ((𝑌𝑉𝑋𝑉) → (𝑅 · (𝑋 + 𝑌)) = ((𝑅 · 𝑋) + (𝑅 · 𝑌))))
1312anabsan2 673 . . . 4 ((𝑊 ∈ LMod ∧ 𝑅𝐾) → ((𝑌𝑉𝑋𝑉) → (𝑅 · (𝑋 + 𝑌)) = ((𝑅 · 𝑋) + (𝑅 · 𝑌))))
1413exp4b 430 . . 3 (𝑊 ∈ LMod → (𝑅𝐾 → (𝑌𝑉 → (𝑋𝑉 → (𝑅 · (𝑋 + 𝑌)) = ((𝑅 · 𝑋) + (𝑅 · 𝑌))))))
1514com34 91 . 2 (𝑊 ∈ LMod → (𝑅𝐾 → (𝑋𝑉 → (𝑌𝑉 → (𝑅 · (𝑋 + 𝑌)) = ((𝑅 · 𝑋) + (𝑅 · 𝑌))))))
16153imp2 1347 1 ((𝑊 ∈ LMod ∧ (𝑅𝐾𝑋𝑉𝑌𝑉)) → (𝑅 · (𝑋 + 𝑌)) = ((𝑅 · 𝑋) + (𝑅 · 𝑌)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1085   = wceq 1534  wcel 2099  cfv 6548  (class class class)co 7420  Basecbs 17179  +gcplusg 17232  .rcmulr 17233  Scalarcsca 17235   ·𝑠 cvsca 17236  1rcur 20120  LModclmod 20742
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-nul 5306
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-ral 3059  df-rab 3430  df-v 3473  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-iota 6500  df-fv 6556  df-ov 7423  df-lmod 20744
This theorem is referenced by:  lmodcom  20790  lmodsubdi  20801  lmodvsghm  20805  islss3  20842  prdslmodd  20852  lmodvsinv2  20921  lmhmplusg  20928  lsmcl  20967  pj1lmhm  20984  lspfixed  21015  lspsolvlem  21029  clmvsdi  25018  cvsi  25056  eqgvscpbl  33062  imaslmod  33065  lshpkrlem4  38585  baerlem5alem1  41181  baerlem5blem1  41182  hdmap14lem8  41348  mendlmod  42617  lmodvsmdi  47446
  Copyright terms: Public domain W3C validator