Metamath Proof Explorer

Theorem lmodsubdir

Description: Scalar multiplication distributive law for subtraction. ( hvsubdistr2 analog.) (Contributed by NM, 2-Jul-2014)

Ref Expression
Hypotheses lmodsubdir.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lmodsubdir.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
lmodsubdir.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lmodsubdir.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
lmodsubdir.m ⊢ − = ( -g ‘ 𝑊 )
lmodsubdir.s ⊢ 𝑆 = ( -g ‘ 𝐹 )
lmodsubdir.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lmodsubdir.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
lmodsubdir.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
lmodsubdir.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion lmodsubdir ( 𝜑 → ( ( 𝐴 𝑆 𝐵 ) · 𝑋 ) = ( ( 𝐴 · 𝑋 ) − ( 𝐵 · 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 lmodsubdir.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lmodsubdir.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
3 lmodsubdir.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4 lmodsubdir.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
5 lmodsubdir.m ⊢ − = ( -g ‘ 𝑊 )
6 lmodsubdir.s ⊢ 𝑆 = ( -g ‘ 𝐹 )
7 lmodsubdir.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
8 lmodsubdir.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
9 lmodsubdir.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
10 lmodsubdir.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
11 3 lmodring ⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Ring )
12 7 11 syl ⊢ ( 𝜑 → 𝐹 ∈ Ring )
13 ringgrp ⊢ ( 𝐹 ∈ Ring → 𝐹 ∈ Grp )
14 12 13 syl ⊢ ( 𝜑 → 𝐹 ∈ Grp )
15 eqid ⊢ ( invg ‘ 𝐹 ) = ( invg ‘ 𝐹 )
16 4 15 grpinvcl ⊢ ( ( 𝐹 ∈ Grp ∧ 𝐵 ∈ 𝐾 ) → ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) ∈ 𝐾 )
17 14 9 16 syl2anc ⊢ ( 𝜑 → ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) ∈ 𝐾 )
18 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
19 eqid ⊢ ( +g ‘ 𝐹 ) = ( +g ‘ 𝐹 )
20 1 18 3 2 4 19 lmodvsdir ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐴 ∈ 𝐾 ∧ ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝐴 ( +g ‘ 𝐹 ) ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) ) · 𝑋 ) = ( ( 𝐴 · 𝑋 ) ( +g ‘ 𝑊 ) ( ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) · 𝑋 ) ) )
21 7 8 17 10 20 syl13anc ⊢ ( 𝜑 → ( ( 𝐴 ( +g ‘ 𝐹 ) ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) ) · 𝑋 ) = ( ( 𝐴 · 𝑋 ) ( +g ‘ 𝑊 ) ( ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) · 𝑋 ) ) )
22 eqid ⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
23 eqid ⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 )
24 4 22 23 15 12 9 ringnegl ⊢ ( 𝜑 → ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) ( .r ‘ 𝐹 ) 𝐵 ) = ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) )
25 24 oveq1d ⊢ ( 𝜑 → ( ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) ( .r ‘ 𝐹 ) 𝐵 ) · 𝑋 ) = ( ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) · 𝑋 ) )
26 4 23 ringidcl ⊢ ( 𝐹 ∈ Ring → ( 1r ‘ 𝐹 ) ∈ 𝐾 )
27 12 26 syl ⊢ ( 𝜑 → ( 1r ‘ 𝐹 ) ∈ 𝐾 )
28 4 15 grpinvcl ⊢ ( ( 𝐹 ∈ Grp ∧ ( 1r ‘ 𝐹 ) ∈ 𝐾 ) → ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) ∈ 𝐾 )
29 14 27 28 syl2anc ⊢ ( 𝜑 → ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) ∈ 𝐾 )
30 1 3 2 4 22 lmodvsass ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) ( .r ‘ 𝐹 ) 𝐵 ) · 𝑋 ) = ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · ( 𝐵 · 𝑋 ) ) )
31 7 29 9 10 30 syl13anc ⊢ ( 𝜑 → ( ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) ( .r ‘ 𝐹 ) 𝐵 ) · 𝑋 ) = ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · ( 𝐵 · 𝑋 ) ) )
32 25 31 eqtr3d ⊢ ( 𝜑 → ( ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) · 𝑋 ) = ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · ( 𝐵 · 𝑋 ) ) )
33 32 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) ( +g ‘ 𝑊 ) ( ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) · 𝑋 ) ) = ( ( 𝐴 · 𝑋 ) ( +g ‘ 𝑊 ) ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · ( 𝐵 · 𝑋 ) ) ) )
34 21 33 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 ( +g ‘ 𝐹 ) ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) ) · 𝑋 ) = ( ( 𝐴 · 𝑋 ) ( +g ‘ 𝑊 ) ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · ( 𝐵 · 𝑋 ) ) ) )
35 4 19 15 6 grpsubval ⊢ ( ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) → ( 𝐴 𝑆 𝐵 ) = ( 𝐴 ( +g ‘ 𝐹 ) ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) ) )
36 8 9 35 syl2anc ⊢ ( 𝜑 → ( 𝐴 𝑆 𝐵 ) = ( 𝐴 ( +g ‘ 𝐹 ) ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) ) )
37 36 oveq1d ⊢ ( 𝜑 → ( ( 𝐴 𝑆 𝐵 ) · 𝑋 ) = ( ( 𝐴 ( +g ‘ 𝐹 ) ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) ) · 𝑋 ) )
38 1 3 2 4 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐴 · 𝑋 ) ∈ 𝑉 )
39 7 8 10 38 syl3anc ⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) ∈ 𝑉 )
40 1 3 2 4 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐵 · 𝑋 ) ∈ 𝑉 )
41 7 9 10 40 syl3anc ⊢ ( 𝜑 → ( 𝐵 · 𝑋 ) ∈ 𝑉 )
42 1 18 5 3 2 15 23 lmodvsubval2 ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐴 · 𝑋 ) ∈ 𝑉 ∧ ( 𝐵 · 𝑋 ) ∈ 𝑉 ) → ( ( 𝐴 · 𝑋 ) − ( 𝐵 · 𝑋 ) ) = ( ( 𝐴 · 𝑋 ) ( +g ‘ 𝑊 ) ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · ( 𝐵 · 𝑋 ) ) ) )
43 7 39 41 42 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) − ( 𝐵 · 𝑋 ) ) = ( ( 𝐴 · 𝑋 ) ( +g ‘ 𝑊 ) ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · ( 𝐵 · 𝑋 ) ) ) )
44 34 37 43 3eqtr4d ⊢ ( 𝜑 → ( ( 𝐴 𝑆 𝐵 ) · 𝑋 ) = ( ( 𝐴 · 𝑋 ) − ( 𝐵 · 𝑋 ) ) )