Theorem nvinv

Description: Minus 1 times a vector is the underlying group's inverse element. Equation 2 of Kreyszig p. 51. (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		nvinv.1	|- X = ( BaseSet ` U )
2		nvinv.2	|- G = ( +v ` U )
3		nvinv.4	|- S = ( .sOLD ` U )
4		nvinv.5	|- M = ( inv ` G )
5		eqid	|- ( 1st ` U ) = ( 1st ` U )
6	5	nvvc	|- ( U e. NrmCVec -> ( 1st ` U ) e. CVecOLD )
7	2	vafval	|- G = ( 1st ` ( 1st ` U ) )
8	3	smfval	|- S = ( 2nd ` ( 1st ` U ) )
9	1 2	bafval	|- X = ran G
10	7 8 9 4	vcm	|- ( ( ( 1st ` U ) e. CVecOLD /\ A e. X ) -> ( -u 1 S A ) = ( M ` A ) )
11	6 10	sylan	|- ( ( U e. NrmCVec /\ A e. X ) -> ( -u 1 S A ) = ( M ` A ) )