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

Theorem lmodvsass 20902
Description: Associative law for scalar product. (ax-hvmulass 31036 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 2735 . . . . . . 7 (+g𝑊) = (+g𝑊)
3 lmodvsass.s . . . . . . 7 · = ( ·𝑠𝑊)
4 lmodvsass.f . . . . . . 7 𝐹 = (Scalar‘𝑊)
5 lmodvsass.k . . . . . . 7 𝐾 = (Base‘𝐹)
6 eqid 2735 . . . . . . 7 (+g𝐹) = (+g𝐹)
7 lmodvsass.t . . . . . . 7 × = (.r𝐹)
8 eqid 2735 . . . . . . 7 (1r𝐹) = (1r𝐹)
91, 2, 3, 4, 5, 6, 7, 8lmodlema 20880 . . . . . 6 ((𝑊 ∈ LMod ∧ (𝑄𝐾𝑅𝐾) ∧ (𝑋𝑉𝑋𝑉)) → (((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g𝑊)𝑋)) = ((𝑅 · 𝑋)(+g𝑊)(𝑅 · 𝑋)) ∧ ((𝑄(+g𝐹)𝑅) · 𝑋) = ((𝑄 · 𝑋)(+g𝑊)(𝑅 · 𝑋))) ∧ (((𝑄 × 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋)) ∧ ((1r𝐹) · 𝑋) = 𝑋)))
109simprld 772 . . . . 5 ((𝑊 ∈ LMod ∧ (𝑄𝐾𝑅𝐾) ∧ (𝑋𝑉𝑋𝑉)) → ((𝑄 × 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋)))
11103expa 1117 . . . 4 (((𝑊 ∈ LMod ∧ (𝑄𝐾𝑅𝐾)) ∧ (𝑋𝑉𝑋𝑉)) → ((𝑄 × 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋)))
1211anabsan2 674 . . 3 (((𝑊 ∈ LMod ∧ (𝑄𝐾𝑅𝐾)) ∧ 𝑋𝑉) → ((𝑄 × 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋)))
1312exp42 435 . 2 (𝑊 ∈ LMod → (𝑄𝐾 → (𝑅𝐾 → (𝑋𝑉 → ((𝑄 × 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋))))))
14133imp2 1348 1 ((𝑊 ∈ LMod ∧ (𝑄𝐾𝑅𝐾𝑋𝑉)) → ((𝑄 × 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086   = wceq 1537  wcel 2106  cfv 6563  (class class class)co 7431  Basecbs 17245  +gcplusg 17298  .rcmulr 17299  Scalarcsca 17301   ·𝑠 cvsca 17302  1rcur 20199  LModclmod 20875
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-nul 5312
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rab 3434  df-v 3480  df-sbc 3792  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434  df-lmod 20877
This theorem is referenced by:  lmodvs0  20911  lmodvsneg  20921  lmodsubvs  20933  lmodsubdi  20934  lmodsubdir  20935  islss3  20975  lss1d  20979  prdslmodd  20985  lmodvsinv  21053  lmhmvsca  21062  lvecvs0or  21128  lssvs0or  21130  lvecinv  21133  lspsnvs  21134  lspfixed  21148  lspsolvlem  21162  lspsolv  21163  frlmup1  21836  assa2ass  21901  assa2ass2  21902  ascldimul  21926  assamulgscmlem2  21938  mplmon2mul  22111  smatvscl  22546  matinv  22699  clmvsass  25136  cvsi  25177  imaslmod  33361  lshpkrlem4  39095  lcdvsass  41590  baerlem3lem1  41690  hgmapmul  41878  prjspertr  42592  prjspner1  42613  mendlmod  43178  lincscm  48276  ldepsprlem  48318  lincresunit3lem3  48320  lincresunit3lem1  48325
  Copyright terms: Public domain W3C validator