Theorem lmodvsass 21058

Description: Associative law for scalar product. (ax-hvmulass 31430 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 2765	. . . . . . 7 ⊢ (+g‘𝑊) = (+g‘𝑊)
3		lmodvsass.s	. . . . . . 7 ⊢ · = ( ·𝑠 ‘𝑊)
4		lmodvsass.f	. . . . . . 7 ⊢ 𝐹 = (Scalar‘𝑊)
5		lmodvsass.k	. . . . . . 7 ⊢ 𝐾 = (Base‘𝐹)
6		eqid 2765	. . . . . . 7 ⊢ (+g‘𝐹) = (+g‘𝐹)
7		lmodvsass.t	. . . . . . 7 ⊢ × = (.r‘𝐹)
8		eqid 2765	. . . . . . 7 ⊢ (1r‘𝐹) = (1r‘𝐹)
9	1, 2, 3, 4, 5, 6, 7, 8	lmodlema 21036	. . . . . 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 2146  ‘cfv 6540  (class class class)co 7419  Basecbs 17291  +_gcplusg 17332  ._rcmulr 17333  Scalarcsca 17335   ·_𝑠 cvsca 17336  1_rcur 20307  LModclmod 21031

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 2148  ax-9 2156  ax-ext 2737  ax-nul 5271

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 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rab 3419  df-v 3459  df-sbc 3747  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-lmod 21033

This theorem is used by:  lmodvs0  21067  lmodvsneg  21077  lmodsubvs  21089  lmodsubdi  21090  lmodsubdir  21091  islss3  21130  lss1d  21134  prdslmodd  21140  lmodvsinv  21207  lmhmvsca  21216  lvecvs0or  21282  lssvs0or  21284  lvecinv  21287  lspsnvs  21288  lspfixed  21302  lspsolvlem  21316  lspsolv  21317  frlmup1  21998  assa2ass  22063  assa2ass2  22064  ascldimul  22088  assamulgscmlem2  22100  mplmon2mul  22270  smatvscl  22731  matinv  22884  clmvsass  25299  cvsi  25340  imaslmod  33737  vietalem  34033  lshpkrlem4  39945  lcdvsass  42439  baerlem3lem1  42539  hgmapmul  42727  prjspertr  43395  prjspner1  43416  mendlmod  43974  lincscm  49267  ldepsprlem  49309  lincresunit3lem3  49311  lincresunit3lem1  49316