Step |
Hyp |
Ref |
Expression |
1 |
|
nvinvfval.2 |
|- G = ( +v ` U ) |
2 |
|
nvinvfval.4 |
|- S = ( .sOLD ` U ) |
3 |
|
nvinvfval.3 |
|- N = ( S o. `' ( 2nd |` ( { -u 1 } X. _V ) ) ) |
4 |
|
eqid |
|- ( BaseSet ` U ) = ( BaseSet ` U ) |
5 |
4 2
|
nvsf |
|- ( U e. NrmCVec -> S : ( CC X. ( BaseSet ` U ) ) --> ( BaseSet ` U ) ) |
6 |
|
neg1cn |
|- -u 1 e. CC |
7 |
3
|
curry1f |
|- ( ( S : ( CC X. ( BaseSet ` U ) ) --> ( BaseSet ` U ) /\ -u 1 e. CC ) -> N : ( BaseSet ` U ) --> ( BaseSet ` U ) ) |
8 |
5 6 7
|
sylancl |
|- ( U e. NrmCVec -> N : ( BaseSet ` U ) --> ( BaseSet ` U ) ) |
9 |
8
|
ffnd |
|- ( U e. NrmCVec -> N Fn ( BaseSet ` U ) ) |
10 |
1
|
nvgrp |
|- ( U e. NrmCVec -> G e. GrpOp ) |
11 |
4 1
|
bafval |
|- ( BaseSet ` U ) = ran G |
12 |
|
eqid |
|- ( inv ` G ) = ( inv ` G ) |
13 |
11 12
|
grpoinvf |
|- ( G e. GrpOp -> ( inv ` G ) : ( BaseSet ` U ) -1-1-onto-> ( BaseSet ` U ) ) |
14 |
|
f1ofn |
|- ( ( inv ` G ) : ( BaseSet ` U ) -1-1-onto-> ( BaseSet ` U ) -> ( inv ` G ) Fn ( BaseSet ` U ) ) |
15 |
10 13 14
|
3syl |
|- ( U e. NrmCVec -> ( inv ` G ) Fn ( BaseSet ` U ) ) |
16 |
5
|
ffnd |
|- ( U e. NrmCVec -> S Fn ( CC X. ( BaseSet ` U ) ) ) |
17 |
16
|
adantr |
|- ( ( U e. NrmCVec /\ x e. ( BaseSet ` U ) ) -> S Fn ( CC X. ( BaseSet ` U ) ) ) |
18 |
3
|
curry1val |
|- ( ( S Fn ( CC X. ( BaseSet ` U ) ) /\ -u 1 e. CC ) -> ( N ` x ) = ( -u 1 S x ) ) |
19 |
17 6 18
|
sylancl |
|- ( ( U e. NrmCVec /\ x e. ( BaseSet ` U ) ) -> ( N ` x ) = ( -u 1 S x ) ) |
20 |
4 1 2 12
|
nvinv |
|- ( ( U e. NrmCVec /\ x e. ( BaseSet ` U ) ) -> ( -u 1 S x ) = ( ( inv ` G ) ` x ) ) |
21 |
19 20
|
eqtrd |
|- ( ( U e. NrmCVec /\ x e. ( BaseSet ` U ) ) -> ( N ` x ) = ( ( inv ` G ) ` x ) ) |
22 |
9 15 21
|
eqfnfvd |
|- ( U e. NrmCVec -> N = ( inv ` G ) ) |