Theorem nvmval

Description: Value of vector subtraction on a normed complex vector space. (Contributed by NM, 11-Sep-2007) (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	nvmval	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A M B ) = ( A G ( -u 1 S B ) ) )

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	2	nvgrp	|- ( U e. NrmCVec -> G e. GrpOp )
6	1 2	bafval	|- X = ran G
7		eqid	|- ( inv ` G ) = ( inv ` G )
8		eqid	|- ( /g ` G ) = ( /g ` G )
9	6 7 8	grpodivval	|- ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A ( /g ` G ) B ) = ( A G ( ( inv ` G ) ` B ) ) )
10	5 9	syl3an1	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A ( /g ` G ) B ) = ( A G ( ( inv ` G ) ` B ) ) )
11	1 2 4 8	nvm	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A M B ) = ( A ( /g ` G ) B ) )
12	1 2 3 7	nvinv	|- ( ( U e. NrmCVec /\ B e. X ) -> ( -u 1 S B ) = ( ( inv ` G ) ` B ) )
13	12	3adant2	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( -u 1 S B ) = ( ( inv ` G ) ` B ) )
14	13	oveq2d	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G ( -u 1 S B ) ) = ( A G ( ( inv ` G ) ` B ) ) )
15	10 11 14	3eqtr4d	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A M B ) = ( A G ( -u 1 S B ) ) )