MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lmodvsdir Structured version   Visualization version   GIF version
Theorem lmodvsdir 20641
Description: Distributive law for scalar product (right-distributivity). (ax-hvdistr1 30525 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 2731 . . . . . . . 8 (.rβ€˜πΉ) = (.rβ€˜πΉ)
8 eqid 2731 . . . . . . . 8 (1rβ€˜πΉ) = (1rβ€˜πΉ)
91, 2, 3, 4, 5, 6, 7, 8lmodlema 20620 . . . . . . 7 ((π‘Š ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) β†’ (((𝑅 Β· 𝑋) ∈ 𝑉 ∧ (𝑅 Β· (𝑋 + 𝑋)) = ((𝑅 Β· 𝑋) + (𝑅 Β· 𝑋)) ∧ ((𝑄 ⨣ 𝑅) Β· 𝑋) = ((𝑄 Β· 𝑋) + (𝑅 Β· 𝑋))) ∧ (((𝑄(.rβ€˜πΉ)𝑅) Β· 𝑋) = (𝑄 Β· (𝑅 Β· 𝑋)) ∧ ((1rβ€˜πΉ) Β· 𝑋) = 𝑋)))
109simpld 494 . . . . . 6 ((π‘Š ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) β†’ ((𝑅 Β· 𝑋) ∈ 𝑉 ∧ (𝑅 Β· (𝑋 + 𝑋)) = ((𝑅 Β· 𝑋) + (𝑅 Β· 𝑋)) ∧ ((𝑄 ⨣ 𝑅) Β· 𝑋) = ((𝑄 Β· 𝑋) + (𝑅 Β· 𝑋))))
1110simp3d 1143 . . . . 5 ((π‘Š ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) β†’ ((𝑄 ⨣ 𝑅) Β· 𝑋) = ((𝑄 Β· 𝑋) + (𝑅 Β· 𝑋)))
12113expa 1117 . . . 4 (((π‘Š ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) β†’ ((𝑄 ⨣ 𝑅) Β· 𝑋) = ((𝑄 Β· 𝑋) + (𝑅 Β· 𝑋)))
1312anabsan2 671 . . 3 (((π‘Š ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾)) ∧ 𝑋 ∈ 𝑉) β†’ ((𝑄 ⨣ 𝑅) Β· 𝑋) = ((𝑄 Β· 𝑋) + (𝑅 Β· 𝑋)))
1413exp42 435 . 2 (π‘Š ∈ LMod β†’ (𝑄 ∈ 𝐾 β†’ (𝑅 ∈ 𝐾 β†’ (𝑋 ∈ 𝑉 β†’ ((𝑄 ⨣ 𝑅) Β· 𝑋) = ((𝑄 Β· 𝑋) + (𝑅 Β· 𝑋))))))
15143imp2 1348 1 ((π‘Š ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) β†’ ((𝑄 ⨣ 𝑅) Β· 𝑋) = ((𝑄 Β· 𝑋) + (𝑅 Β· 𝑋)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105  β€˜cfv 6544  (class class class)co 7412  Basecbs 17149  +gcplusg 17202  .rcmulr 17203  Scalarcsca 17205   ·𝑠 cvsca 17206  1rcur 20076  LModclmod 20615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-nul 5307
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rab 3432  df-v 3475  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7415  df-lmod 20617
This theorem is referenced by:  lmod0vs  20650  lmodvsmmulgdi  20652  lmodvneg1  20660  lmodcom  20663  lmodsubdir  20675  islss3  20715  lss1d  20719  prdslmodd  20725  lspsolvlem  20901  frlmup1  21573  asclghm  21657  scmataddcl  22239  scmatghm  22256  pm2mpghm  22539  clmvsdir  24839  cvsi  24878  lmodvslmhm  32469  imaslmod  32735  lshpkrlem4  38287  baerlem3lem1  40882  baerlem5blem1  40884  hgmapadd  41069  mendlmod  42238  lmodvsmdi  47148  lincsum  47199  ldepsprlem  47242
  Copyright terms: Public domain W3C validator