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

Theorem lmodvsass 20347
Description: Associative law for scalar product. (ax-hvmulass 29949 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
Hypotheses
Ref Expression
lmodvsass.v 𝑉 = (Baseβ€˜π‘Š)
lmodvsass.f 𝐹 = (Scalarβ€˜π‘Š)
lmodvsass.s Β· = ( ·𝑠 β€˜π‘Š)
lmodvsass.k 𝐾 = (Baseβ€˜πΉ)
lmodvsass.t Γ— = (.rβ€˜πΉ)
Assertion
Ref Expression
lmodvsass ((π‘Š ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) β†’ ((𝑄 Γ— 𝑅) Β· 𝑋) = (𝑄 Β· (𝑅 Β· 𝑋)))

Proof of Theorem lmodvsass
StepHypRef Expression
1 lmodvsass.v . . . . . . 7 𝑉 = (Baseβ€˜π‘Š)
2 eqid 2736 . . . . . . 7 (+gβ€˜π‘Š) = (+gβ€˜π‘Š)
3 lmodvsass.s . . . . . . 7 Β· = ( ·𝑠 β€˜π‘Š)
4 lmodvsass.f . . . . . . 7 𝐹 = (Scalarβ€˜π‘Š)
5 lmodvsass.k . . . . . . 7 𝐾 = (Baseβ€˜πΉ)
6 eqid 2736 . . . . . . 7 (+gβ€˜πΉ) = (+gβ€˜πΉ)
7 lmodvsass.t . . . . . . 7 Γ— = (.rβ€˜πΉ)
8 eqid 2736 . . . . . . 7 (1rβ€˜πΉ) = (1rβ€˜πΉ)
91, 2, 3, 4, 5, 6, 7, 8lmodlema 20327 . . . . . 6 ((π‘Š ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) β†’ (((𝑅 Β· 𝑋) ∈ 𝑉 ∧ (𝑅 Β· (𝑋(+gβ€˜π‘Š)𝑋)) = ((𝑅 Β· 𝑋)(+gβ€˜π‘Š)(𝑅 Β· 𝑋)) ∧ ((𝑄(+gβ€˜πΉ)𝑅) Β· 𝑋) = ((𝑄 Β· 𝑋)(+gβ€˜π‘Š)(𝑅 Β· 𝑋))) ∧ (((𝑄 Γ— 𝑅) Β· 𝑋) = (𝑄 Β· (𝑅 Β· 𝑋)) ∧ ((1rβ€˜πΉ) Β· 𝑋) = 𝑋)))
109simprld 770 . . . . 5 ((π‘Š ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) β†’ ((𝑄 Γ— 𝑅) Β· 𝑋) = (𝑄 Β· (𝑅 Β· 𝑋)))
11103expa 1118 . . . 4 (((π‘Š ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) β†’ ((𝑄 Γ— 𝑅) Β· 𝑋) = (𝑄 Β· (𝑅 Β· 𝑋)))
1211anabsan2 672 . . 3 (((π‘Š ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾)) ∧ 𝑋 ∈ 𝑉) β†’ ((𝑄 Γ— 𝑅) Β· 𝑋) = (𝑄 Β· (𝑅 Β· 𝑋)))
1312exp42 436 . 2 (π‘Š ∈ LMod β†’ (𝑄 ∈ 𝐾 β†’ (𝑅 ∈ 𝐾 β†’ (𝑋 ∈ 𝑉 β†’ ((𝑄 Γ— 𝑅) Β· 𝑋) = (𝑄 Β· (𝑅 Β· 𝑋))))))
14133imp2 1349 1 ((π‘Š ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) β†’ ((𝑄 Γ— 𝑅) Β· 𝑋) = (𝑄 Β· (𝑅 Β· 𝑋)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  β€˜cfv 6496  (class class class)co 7357  Basecbs 17083  +gcplusg 17133  .rcmulr 17134  Scalarcsca 17136   ·𝑠 cvsca 17137  1rcur 19913  LModclmod 20322
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-nul 5263
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rab 3408  df-v 3447  df-sbc 3740  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-iota 6448  df-fv 6504  df-ov 7360  df-lmod 20324
This theorem is referenced by:  lmodvs0  20356  lmodvsneg  20366  lmodsubvs  20378  lmodsubdi  20379  lmodsubdir  20380  islss3  20420  lss1d  20424  prdslmodd  20430  lmodvsinv  20497  lmhmvsca  20506  lvecvs0or  20569  lssvs0or  20571  lvecinv  20574  lspsnvs  20575  lspfixed  20589  lspsolvlem  20603  lspsolv  20604  frlmup1  21204  assa2ass  21269  ascldimul  21291  assamulgscmlem2  21303  mplmon2mul  21477  smatvscl  21873  matinv  22026  clmvsass  24452  cvsi  24493  imaslmod  32145  lshpkrlem4  37575  lcdvsass  40070  baerlem3lem1  40170  hgmapmul  40358  prjspertr  40929  prjspner1  40950  mendlmod  41506  lincscm  46501  ldepsprlem  46543  lincresunit3lem3  46545  lincresunit3lem1  46550
  Copyright terms: Public domain W3C validator