Metamath Proof Explorer

Theorem lmodsubvs

Description: Subtraction of a scalar product in terms of addition. (Contributed by NM, 9-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 lmodsubvs.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lmodsubvs.p ⊢ + = ( +g ‘ 𝑊 )
3 lmodsubvs.m ⊢ − = ( -g ‘ 𝑊 )
4 lmodsubvs.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
5 lmodsubvs.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
6 lmodsubvs.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
7 lmodsubvs.n ⊢ 𝑁 = ( invg ‘ 𝐹 )
8 lmodsubvs.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
9 lmodsubvs.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
10 lmodsubvs.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
11 lmodsubvs.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
12 1 5 4 6 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝐴 · 𝑌 ) ∈ 𝑉 )
13 8 9 11 12 syl3anc ⊢ ( 𝜑 → ( 𝐴 · 𝑌 ) ∈ 𝑉 )
14 eqid ⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 )
15 1 2 3 5 4 7 14 lmodvsubval2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ ( 𝐴 · 𝑌 ) ∈ 𝑉 ) → ( 𝑋 − ( 𝐴 · 𝑌 ) ) = ( 𝑋 + ( ( 𝑁 ‘ ( 1r ‘ 𝐹 ) ) · ( 𝐴 · 𝑌 ) ) ) )
16 8 10 13 15 syl3anc ⊢ ( 𝜑 → ( 𝑋 − ( 𝐴 · 𝑌 ) ) = ( 𝑋 + ( ( 𝑁 ‘ ( 1r ‘ 𝐹 ) ) · ( 𝐴 · 𝑌 ) ) ) )
17 5 lmodring ⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Ring )
18 8 17 syl ⊢ ( 𝜑 → 𝐹 ∈ Ring )
19 ringgrp ⊢ ( 𝐹 ∈ Ring → 𝐹 ∈ Grp )
20 18 19 syl ⊢ ( 𝜑 → 𝐹 ∈ Grp )
21 6 14 ringidcl ⊢ ( 𝐹 ∈ Ring → ( 1r ‘ 𝐹 ) ∈ 𝐾 )
22 18 21 syl ⊢ ( 𝜑 → ( 1r ‘ 𝐹 ) ∈ 𝐾 )
23 6 7 grpinvcl ⊢ ( ( 𝐹 ∈ Grp ∧ ( 1r ‘ 𝐹 ) ∈ 𝐾 ) → ( 𝑁 ‘ ( 1r ‘ 𝐹 ) ) ∈ 𝐾 )
24 20 22 23 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ ( 1r ‘ 𝐹 ) ) ∈ 𝐾 )
25 eqid ⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
26 1 5 4 6 25 lmodvsass ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑁 ‘ ( 1r ‘ 𝐹 ) ) ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( 𝑁 ‘ ( 1r ‘ 𝐹 ) ) ( .r ‘ 𝐹 ) 𝐴 ) · 𝑌 ) = ( ( 𝑁 ‘ ( 1r ‘ 𝐹 ) ) · ( 𝐴 · 𝑌 ) ) )
27 8 24 9 11 26 syl13anc ⊢ ( 𝜑 → ( ( ( 𝑁 ‘ ( 1r ‘ 𝐹 ) ) ( .r ‘ 𝐹 ) 𝐴 ) · 𝑌 ) = ( ( 𝑁 ‘ ( 1r ‘ 𝐹 ) ) · ( 𝐴 · 𝑌 ) ) )
28 6 25 14 7 18 9 ringnegl ⊢ ( 𝜑 → ( ( 𝑁 ‘ ( 1r ‘ 𝐹 ) ) ( .r ‘ 𝐹 ) 𝐴 ) = ( 𝑁 ‘ 𝐴 ) )
29 28 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑁 ‘ ( 1r ‘ 𝐹 ) ) ( .r ‘ 𝐹 ) 𝐴 ) · 𝑌 ) = ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) )
30 27 29 eqtr3d ⊢ ( 𝜑 → ( ( 𝑁 ‘ ( 1r ‘ 𝐹 ) ) · ( 𝐴 · 𝑌 ) ) = ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) )
31 30 oveq2d ⊢ ( 𝜑 → ( 𝑋 + ( ( 𝑁 ‘ ( 1r ‘ 𝐹 ) ) · ( 𝐴 · 𝑌 ) ) ) = ( 𝑋 + ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) )
32 16 31 eqtrd ⊢ ( 𝜑 → ( 𝑋 − ( 𝐴 · 𝑌 ) ) = ( 𝑋 + ( ( 𝑁 ‘ 𝐴 ) · 𝑌 ) ) )