Metamath Proof Explorer

Theorem nvinvfval

Description: Function for the negative of a vector on a normed complex vector space, in terms of the underlying addition group inverse. (We currently do not have a separate notation for the negative of a vector.) (Contributed by NM, 27-Mar-2008) (New usage is discouraged.)

Ref Expression
Hypotheses nvinvfval.2 
|- G = ( +v ` U )
nvinvfval.4 
|- S = ( .sOLD ` U )
nvinvfval.3 
|- N = ( S o. `' ( 2nd |` ( { -u 1 } X. _V ) ) )
Assertion nvinvfval 
|- ( U e. NrmCVec -> N = ( inv ` G ) )

Proof

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