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 )