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 ) |