This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )