Theorem lmodvsass 21071

Description: Associative law for scalar product. (ax-hvmulass 31488 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

Step	Hyp	Ref	Expression
1		lmodvsass.v	. . . . . . 7 ⊢ 𝑉 = (Base‘𝑊)
2		eqid 2760	. . . . . . 7 ⊢ (+g‘𝑊) = (+g‘𝑊)
3		lmodvsass.s	. . . . . . 7 ⊢ · = ( ·𝑠 ‘𝑊)
4		lmodvsass.f	. . . . . . 7 ⊢ 𝐹 = (Scalar‘𝑊)
5		lmodvsass.k	. . . . . . 7 ⊢ 𝐾 = (Base‘𝐹)
6		eqid 2760	. . . . . . 7 ⊢ (+g‘𝐹) = (+g‘𝐹)
7		lmodvsass.t	. . . . . . 7 ⊢ × = (.r‘𝐹)
8		eqid 2760	. . . . . . 7 ⊢ (1r‘𝐹) = (1r‘𝐹)
9	1, 2, 3, 4, 5, 6, 7, 8	lmodlema 21049	. . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g‘𝑊)𝑋)) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)) ∧ ((𝑄(+g‘𝐹)𝑅) · 𝑋) = ((𝑄 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) ∧ (((𝑄 × 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋)) ∧ ((1r‘𝐹) · 𝑋) = 𝑋)))
10	9	simprld 784	. . . . 5 ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 × 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋)))
11	10	3expa 1136	. . . 4 ⊢ (((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 × 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋)))
12	11	anabsan2 687	. . 3 ⊢ (((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾)) ∧ 𝑋 ∈ 𝑉) → ((𝑄 × 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋)))
13	12	exp42 441	. 2 ⊢ (𝑊 ∈ LMod → (𝑄 ∈ 𝐾 → (𝑅 ∈ 𝐾 → (𝑋 ∈ 𝑉 → ((𝑄 × 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋))))))
14	13	3imp2 1368	1 ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 × 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ‘cfv 6533  (class class class)co 7413  Basecbs 17301  +_gcplusg 17342  ._rcmulr 17343  Scalarcsca 17345   ·_𝑠 cvsca 17346  1_rcur 20320  LModclmod 21044

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-nul 5263

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rab 3413  df-v 3452  df-sbc 3740  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7416  df-lmod 21046

This theorem is used by:  lmodvs0  21080  lmodvsneg  21090  lmodsubvs  21102  lmodsubdi  21103  lmodsubdir  21104  islss3  21143  lss1d  21147  prdslmodd  21153  lmodvsinv  21220  lmhmvsca  21229  lvecvs0or  21295  lssvs0or  21297  lvecinv  21300  lspsnvs  21301  lspfixed  21315  lspsolvlem  21329  lspsolv  21330  frlmup1  22011  assa2ass  22078  assa2ass2  22079  ascldimul  22103  assamulgscmlem2  22115  mplmon2mul  22285  smatvscl  22746  matinv  22899  clmvsass  25317  cvsi  25358  imaslmod  33793  vietalem  34089  lshpkrlem4  39986  lcdvsass  42480  baerlem3lem1  42580  hgmapmul  42768  prjspertr  43451  prjspner1  43472  mendlmod  44030  lincscm  49360  ldepsprlem  49402  lincresunit3lem3  49404  lincresunit3lem1  49409