This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lmodsubdi

Description: Scalar multiplication distributive law for subtraction. ( hvsubdistr1 analogue, with longer proof since our scalar multiplication is not commutative.) (Contributed by NM, 2-Jul-2014)

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

Proof

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