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