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

Metamath Proof Explorer

Theorem lmodvsubval2

Description: Value of vector subtraction in terms of addition. ( hvsubval analog.) (Contributed by NM, 31-Mar-2014) (Proof shortened by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lmodvsubval2.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lmodvsubval2.p ⊢ + = ( +g ‘ 𝑊 )
lmodvsubval2.m ⊢ − = ( -g ‘ 𝑊 )
lmodvsubval2.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lmodvsubval2.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
lmodvsubval2.n ⊢ 𝑁 = ( invg ‘ 𝐹 )
lmodvsubval2.u ⊢ 1 = ( 1r ‘ 𝐹 )
Assertion lmodvsubval2 ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 − 𝐵 ) = ( 𝐴 + ( ( 𝑁 ‘ 1 ) · 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 lmodvsubval2.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lmodvsubval2.p ⊢ + = ( +g ‘ 𝑊 )
3 lmodvsubval2.m ⊢ − = ( -g ‘ 𝑊 )
4 lmodvsubval2.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
5 lmodvsubval2.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
6 lmodvsubval2.n ⊢ 𝑁 = ( invg ‘ 𝐹 )
7 lmodvsubval2.u ⊢ 1 = ( 1r ‘ 𝐹 )
8 eqid ⊢ ( invg ‘ 𝑊 ) = ( invg ‘ 𝑊 )
9 1 2 8 3 grpsubval ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 − 𝐵 ) = ( 𝐴 + ( ( invg ‘ 𝑊 ) ‘ 𝐵 ) ) )
10 9 3adant1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 − 𝐵 ) = ( 𝐴 + ( ( invg ‘ 𝑊 ) ‘ 𝐵 ) ) )
11 1 8 4 5 7 6 lmodvneg1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑁 ‘ 1 ) · 𝐵 ) = ( ( invg ‘ 𝑊 ) ‘ 𝐵 ) )
12 11 3adant2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑁 ‘ 1 ) · 𝐵 ) = ( ( invg ‘ 𝑊 ) ‘ 𝐵 ) )
13 12 oveq2d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 + ( ( 𝑁 ‘ 1 ) · 𝐵 ) ) = ( 𝐴 + ( ( invg ‘ 𝑊 ) ‘ 𝐵 ) ) )
14 10 13 eqtr4d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 − 𝐵 ) = ( 𝐴 + ( ( 𝑁 ‘ 1 ) · 𝐵 ) ) )