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

Theorem lmodvsass 19645
Description: Associative law for scalar product. (ax-hvmulass 28779 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 2824 . . . . . . 7 (+g𝑊) = (+g𝑊)
3 lmodvsass.s . . . . . . 7 · = ( ·𝑠𝑊)
4 lmodvsass.f . . . . . . 7 𝐹 = (Scalar‘𝑊)
5 lmodvsass.k . . . . . . 7 𝐾 = (Base‘𝐹)
6 eqid 2824 . . . . . . 7 (+g𝐹) = (+g𝐹)
7 lmodvsass.t . . . . . . 7 × = (.r𝐹)
8 eqid 2824 . . . . . . 7 (1r𝐹) = (1r𝐹)
91, 2, 3, 4, 5, 6, 7, 8lmodlema 19625 . . . . . 6 ((𝑊 ∈ LMod ∧ (𝑄𝐾𝑅𝐾) ∧ (𝑋𝑉𝑋𝑉)) → (((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g𝑊)𝑋)) = ((𝑅 · 𝑋)(+g𝑊)(𝑅 · 𝑋)) ∧ ((𝑄(+g𝐹)𝑅) · 𝑋) = ((𝑄 · 𝑋)(+g𝑊)(𝑅 · 𝑋))) ∧ (((𝑄 × 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋)) ∧ ((1r𝐹) · 𝑋) = 𝑋)))
109simprld 771 . . . . 5 ((𝑊 ∈ LMod ∧ (𝑄𝐾𝑅𝐾) ∧ (𝑋𝑉𝑋𝑉)) → ((𝑄 × 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋)))
11103expa 1115 . . . 4 (((𝑊 ∈ LMod ∧ (𝑄𝐾𝑅𝐾)) ∧ (𝑋𝑉𝑋𝑉)) → ((𝑄 × 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋)))
1211anabsan2 673 . . 3 (((𝑊 ∈ LMod ∧ (𝑄𝐾𝑅𝐾)) ∧ 𝑋𝑉) → ((𝑄 × 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋)))
1312exp42 439 . 2 (𝑊 ∈ LMod → (𝑄𝐾 → (𝑅𝐾 → (𝑋𝑉 → ((𝑄 × 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋))))))
14133imp2 1346 1 ((𝑊 ∈ LMod ∧ (𝑄𝐾𝑅𝐾𝑋𝑉)) → ((𝑄 × 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084   = wceq 1538  wcel 2115  cfv 6336  (class class class)co 7138  Basecbs 16472  +gcplusg 16554  .rcmulr 16555  Scalarcsca 16557   ·𝑠 cvsca 16558  1rcur 19240  LModclmod 19620
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-nul 5191
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3137  df-rex 3138  df-rab 3141  df-v 3481  df-sbc 3758  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-sn 4549  df-pr 4551  df-op 4555  df-uni 4820  df-br 5048  df-iota 6295  df-fv 6344  df-ov 7141  df-lmod 19622
This theorem is referenced by:  lmodvs0  19654  lmodvsneg  19664  lmodsubvs  19676  lmodsubdi  19677  lmodsubdir  19678  islss3  19717  lss1d  19721  prdslmodd  19727  lmodvsinv  19794  lmhmvsca  19803  lvecvs0or  19866  lssvs0or  19868  lvecinv  19871  lspsnvs  19872  lspfixed  19886  lspsolvlem  19900  lspsolv  19901  assa2ass  20081  ascldimul  20102  ascldimulOLD  20103  assamulgscmlem2  20115  mplmon2mul  20267  frlmup1  20928  smatvscl  21119  matinv  21272  clmvsass  23683  cvsi  23724  imaslmod  30940  lshpkrlem4  36309  lcdvsass  38803  baerlem3lem1  38903  hgmapmul  39091  prjspertr  39431  mendlmod  39969  lincscm  44680  ldepsprlem  44722  lincresunit3lem3  44724  lincresunit3lem1  44729
  Copyright terms: Public domain W3C validator