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 
|- V = ( Base ` W )
lmodvsubval2.p 
|- .+ = ( +g ` W )
lmodvsubval2.m 
|- .- = ( -g ` W )
lmodvsubval2.f 
|- F = ( Scalar ` W )
lmodvsubval2.s 
|- .x. = ( .s ` W )
lmodvsubval2.n 
|- N = ( invg ` F )
lmodvsubval2.u 
|- .1. = ( 1r ` F )
Assertion lmodvsubval2 
|- ( ( W e. LMod /\ A e. V /\ B e. V ) -> ( A .- B ) = ( A .+ ( ( N ` .1. ) .x. B ) ) )

Proof

Step Hyp Ref Expression
1 lmodvsubval2.v 
 |-  V = ( Base ` W )
2 lmodvsubval2.p 
 |-  .+ = ( +g ` W )
3 lmodvsubval2.m 
 |-  .- = ( -g ` W )
4 lmodvsubval2.f 
 |-  F = ( Scalar ` W )
5 lmodvsubval2.s 
 |-  .x. = ( .s ` W )
6 lmodvsubval2.n 
 |-  N = ( invg ` F )
7 lmodvsubval2.u 
 |-  .1. = ( 1r ` F )
8 eqid 
 |-  ( invg ` W ) = ( invg ` W )
9 1 2 8 3 grpsubval 
 |-  ( ( A e. V /\ B e. V ) -> ( A .- B ) = ( A .+ ( ( invg ` W ) ` B ) ) )
10 9 3adant1 
 |-  ( ( W e. LMod /\ A e. V /\ B e. V ) -> ( A .- B ) = ( A .+ ( ( invg ` W ) ` B ) ) )
11 1 8 4 5 7 6 lmodvneg1 
 |-  ( ( W e. LMod /\ B e. V ) -> ( ( N ` .1. ) .x. B ) = ( ( invg ` W ) ` B ) )
12 11 3adant2 
 |-  ( ( W e. LMod /\ A e. V /\ B e. V ) -> ( ( N ` .1. ) .x. B ) = ( ( invg ` W ) ` B ) )
13 12 oveq2d 
 |-  ( ( W e. LMod /\ A e. V /\ B e. V ) -> ( A .+ ( ( N ` .1. ) .x. B ) ) = ( A .+ ( ( invg ` W ) ` B ) ) )
14 10 13 eqtr4d 
 |-  ( ( W e. LMod /\ A e. V /\ B e. V ) -> ( A .- B ) = ( A .+ ( ( N ` .1. ) .x. B ) ) )