Theorem nvlinv

Description: Minus a vector plus 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	nvlinv	|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( -u 1 S A ) G 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	grpolinv	|- ( ( G e. GrpOp /\ A e. X ) -> ( ( ( inv ` G ) ` A ) G A ) = ( GId ` G ) )
10	5 9	sylan	|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( ( inv ` G ) ` A ) 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	oveq1d	|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( -u 1 S A ) G A ) = ( ( ( inv ` G ) ` A ) 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 ) -> ( ( -u 1 S A ) G A ) = Z )