Metamath Proof Explorer

Theorem nvnegneg

Description: Double negative of a vector. (Contributed by NM, 4-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nvnegneg.1 
|- X = ( BaseSet ` U )
nvnegneg.4 
|- S = ( .sOLD ` U )
Assertion nvnegneg 
|- ( ( U e. NrmCVec /\ A e. X ) -> ( -u 1 S ( -u 1 S A ) ) = A )

Proof

Step Hyp Ref Expression
1 nvnegneg.1 
 |-  X = ( BaseSet ` U )
2 nvnegneg.4 
 |-  S = ( .sOLD ` U )
3 neg1cn 
 |-  -u 1 e. CC
4 1 2 nvscl 
 |-  ( ( U e. NrmCVec /\ -u 1 e. CC /\ A e. X ) -> ( -u 1 S A ) e. X )
5 3 4 mp3an2 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( -u 1 S A ) e. X )
6 eqid 
 |-  ( +v ` U ) = ( +v ` U )
7 eqid 
 |-  ( inv ` ( +v ` U ) ) = ( inv ` ( +v ` U ) )
8 1 6 2 7 nvinv 
 |-  ( ( U e. NrmCVec /\ ( -u 1 S A ) e. X ) -> ( -u 1 S ( -u 1 S A ) ) = ( ( inv ` ( +v ` U ) ) ` ( -u 1 S A ) ) )
9 5 8 syldan 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( -u 1 S ( -u 1 S A ) ) = ( ( inv ` ( +v ` U ) ) ` ( -u 1 S A ) ) )
10 1 6 2 7 nvinv 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( -u 1 S A ) = ( ( inv ` ( +v ` U ) ) ` A ) )
11 10 fveq2d 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( ( inv ` ( +v ` U ) ) ` ( -u 1 S A ) ) = ( ( inv ` ( +v ` U ) ) ` ( ( inv ` ( +v ` U ) ) ` A ) ) )
12 6 nvgrp 
 |-  ( U e. NrmCVec -> ( +v ` U ) e. GrpOp )
13 1 6 bafval 
 |-  X = ran ( +v ` U )
14 13 7 grpo2inv 
 |-  ( ( ( +v ` U ) e. GrpOp /\ A e. X ) -> ( ( inv ` ( +v ` U ) ) ` ( ( inv ` ( +v ` U ) ) ` A ) ) = A )
15 12 14 sylan 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( ( inv ` ( +v ` U ) ) ` ( ( inv ` ( +v ` U ) ) ` A ) ) = A )
16 9 11 15 3eqtrd 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( -u 1 S ( -u 1 S A ) ) = A )