Theorem nvmval2

Description: Value of vector subtraction on a normed complex vector space. (Contributed by Mario Carneiro, 19-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvmval.1	|- X = ( BaseSet ` U )
	nvmval.2	|- G = ( +v ` U )
	nvmval.4	|- S = ( .sOLD ` U )
	nvmval.3	|- M = ( -v ` U )
Assertion	nvmval2	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A M B ) = ( ( -u 1 S B ) G A ) )

Proof

Step	Hyp	Ref	Expression
1		nvmval.1	|- X = ( BaseSet ` U )
2		nvmval.2	|- G = ( +v ` U )
3		nvmval.4	|- S = ( .sOLD ` U )
4		nvmval.3	|- M = ( -v ` U )
5	1 2 3 4	nvmval	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A M B ) = ( A G ( -u 1 S B ) ) )
6		neg1cn	|- -u 1 e. CC
7	1 3	nvscl	|- ( ( U e. NrmCVec /\ -u 1 e. CC /\ B e. X ) -> ( -u 1 S B ) e. X )
8	6 7	mp3an2	|- ( ( U e. NrmCVec /\ B e. X ) -> ( -u 1 S B ) e. X )
9	8	3adant2	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( -u 1 S B ) e. X )
10	1 2	nvcom	|- ( ( U e. NrmCVec /\ A e. X /\ ( -u 1 S B ) e. X ) -> ( A G ( -u 1 S B ) ) = ( ( -u 1 S B ) G A ) )
11	9 10	syld3an3	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G ( -u 1 S B ) ) = ( ( -u 1 S B ) G A ) )
12	5 11	eqtrd	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A M B ) = ( ( -u 1 S B ) G A ) )