Theorem lmodvsdir 20988

Description: Distributive law for scalar product (right-distributivity). (ax-hvdistr1 31338 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)

Hypotheses

Ref	Expression
lmodvsdir.v	⊢ 𝑉 = (Base‘𝑊)
lmodvsdir.a	⊢ + = (+g‘𝑊)
lmodvsdir.f	⊢ 𝐹 = (Scalar‘𝑊)
lmodvsdir.s	⊢ · = ( ·𝑠 ‘𝑊)
lmodvsdir.k	⊢ 𝐾 = (Base‘𝐹)
lmodvsdir.p	⊢ ⨣ = (+g‘𝐹)

Assertion

Ref	Expression
lmodvsdir	⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 ⨣ 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋)))

Proof of Theorem lmodvsdir

Step	Hyp	Ref	Expression
1		lmodvsdir.v	. . . . . . . 8 ⊢ 𝑉 = (Base‘𝑊)
2		lmodvsdir.a	. . . . . . . 8 ⊢ + = (+g‘𝑊)
3		lmodvsdir.s	. . . . . . . 8 ⊢ · = ( ·𝑠 ‘𝑊)
4		lmodvsdir.f	. . . . . . . 8 ⊢ 𝐹 = (Scalar‘𝑊)
5		lmodvsdir.k	. . . . . . . 8 ⊢ 𝐾 = (Base‘𝐹)
6		lmodvsdir.p	. . . . . . . 8 ⊢ ⨣ = (+g‘𝐹)
7		eqid 2763	. . . . . . . 8 ⊢ (.r‘𝐹) = (.r‘𝐹)
8		eqid 2763	. . . . . . . 8 ⊢ (1r‘𝐹) = (1r‘𝐹)
9	1, 2, 3, 4, 5, 6, 7, 8	lmodlema 20967	. . . . . . 7 ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋 + 𝑋)) = ((𝑅 · 𝑋) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋))) ∧ (((𝑄(.r‘𝐹)𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋)) ∧ ((1r‘𝐹) · 𝑋) = 𝑋)))
10	9	simpld 499	. . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋 + 𝑋)) = ((𝑅 · 𝑋) + (𝑅 · 𝑋)) ∧ ((𝑄 ⨣ 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋))))
11	10	simp3d 1162	. . . . 5 ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 ⨣ 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋)))
12	11	3expa 1136	. . . 4 ⊢ (((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 ⨣ 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋)))
13	12	anabsan2 686	. . 3 ⊢ (((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾)) ∧ 𝑋 ∈ 𝑉) → ((𝑄 ⨣ 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋)))
14	13	exp42 440	. 2 ⊢ (𝑊 ∈ LMod → (𝑄 ∈ 𝐾 → (𝑅 ∈ 𝐾 → (𝑋 ∈ 𝑉 → ((𝑄 ⨣ 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋))))))
15	14	3imp2 1368	1 ⊢ ((𝑊 ∈ LMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 ⨣ 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋)))

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143  ‘cfv 6538  (class class class)co 7412  Basecbs 17270  +_gcplusg 17311  ._rcmulr 17312  Scalarcsca 17314   ·_𝑠 cvsca 17315  1_rcur 20264  LModclmod 20962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5270

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rab 3417  df-v 3457  df-sbc 3746  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415  df-lmod 20964

This theorem is referenced by:  lmod0vs  20997  lmodvsmmulgdi  20999  lmodvneg1  21007  lmodcom  21010  lmodsubdir  21022  islss3  21061  lss1d  21065  prdslmodd  21071  lspsolvlem  21247  frlmup1  21929  asclghm  22013  scmataddcl  22654  scmatghm  22671  pm2mpghm  22954  clmvsdir  25231  cvsi  25270  lmodvslmhm  33348  imaslmod  33651  lshpkrlem4  39865  baerlem3lem1  42459  baerlem5blem1  42461  hgmapadd  42646  mendlmod  43896  lmodvsmdi  49136  lincsum  49186  ldepsprlem  49229