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 ) ) )