Theorem nvrinv

Description: A vector minus itself. (Contributed by NM, 4-Dec-2007) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvrinv.1	|- X = ( BaseSet ` U )
	nvrinv.2	|- G = ( +v ` U )
	nvrinv.4	|- S = ( .sOLD ` U )
	nvrinv.6	|- Z = ( 0vec ` U )
Assertion	nvrinv	|- ( ( U e. NrmCVec /\ A e. X ) -> ( A G ( -u 1 S A ) ) = Z )

Proof

Step	Hyp	Ref	Expression
1		nvrinv.1	|- X = ( BaseSet ` U )
2		nvrinv.2	|- G = ( +v ` U )
3		nvrinv.4	|- S = ( .sOLD ` U )
4		nvrinv.6	|- Z = ( 0vec ` U )
5	2	nvgrp	|- ( U e. NrmCVec -> G e. GrpOp )
6	1 2	bafval	|- X = ran G
7		eqid	|- ( GId ` G ) = ( GId ` G )
8		eqid	|- ( inv ` G ) = ( inv ` G )
9	6 7 8	grporinv	|- ( ( G e. GrpOp /\ A e. X ) -> ( A G ( ( inv ` G ) ` A ) ) = ( GId ` G ) )
10	5 9	sylan	|- ( ( U e. NrmCVec /\ A e. X ) -> ( A G ( ( inv ` G ) ` A ) ) = ( GId ` G ) )
11	1 2 3 8	nvinv	|- ( ( U e. NrmCVec /\ A e. X ) -> ( -u 1 S A ) = ( ( inv ` G ) ` A ) )
12	11	oveq2d	|- ( ( U e. NrmCVec /\ A e. X ) -> ( A G ( -u 1 S A ) ) = ( A G ( ( inv ` G ) ` A ) ) )
13	2 4	0vfval	|- ( U e. NrmCVec -> Z = ( GId ` G ) )
14	13	adantr	|- ( ( U e. NrmCVec /\ A e. X ) -> Z = ( GId ` G ) )
15	10 12 14	3eqtr4d	|- ( ( U e. NrmCVec /\ A e. X ) -> ( A G ( -u 1 S A ) ) = Z )