Metamath Proof Explorer

Theorem nvi

Description: The properties of a normed complex vector space, which is a vector space accompanied by a norm. (Contributed by NM, 11-Nov-2006) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nvi.1 
|- X = ( BaseSet ` U )
nvi.2 
|- G = ( +v ` U )
nvi.4 
|- S = ( .sOLD ` U )
nvi.5 
|- Z = ( 0vec ` U )
nvi.6 
|- N = ( normCV ` U )
Assertion nvi 
|- ( U e. NrmCVec -> ( <. G , S >. e. CVecOLD /\ N : X --> RR /\ A. x e. X ( ( ( N ` x ) = 0 -> x = Z ) /\ A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 nvi.1 
 |-  X = ( BaseSet ` U )
2 nvi.2 
 |-  G = ( +v ` U )
3 nvi.4 
 |-  S = ( .sOLD ` U )
4 nvi.5 
 |-  Z = ( 0vec ` U )
5 nvi.6 
 |-  N = ( normCV ` U )
6 eqid 
 |-  ( 1st ` U ) = ( 1st ` U )
7 6 5 nvop2 
 |-  ( U e. NrmCVec -> U = <. ( 1st ` U ) , N >. )
8 6 2 3 nvvop 
 |-  ( U e. NrmCVec -> ( 1st ` U ) = <. G , S >. )
9 8 opeq1d 
 |-  ( U e. NrmCVec -> <. ( 1st ` U ) , N >. = <. <. G , S >. , N >. )
10 7 9 eqtrd 
 |-  ( U e. NrmCVec -> U = <. <. G , S >. , N >. )
11 id 
 |-  ( U e. NrmCVec -> U e. NrmCVec )
12 10 11 eqeltrrd 
 |-  ( U e. NrmCVec -> <. <. G , S >. , N >. e. NrmCVec )
13 1 2 bafval 
 |-  X = ran G
14 eqid 
 |-  ( GId ` G ) = ( GId ` G )
15 13 14 isnv 
 |-  ( <. <. G , S >. , N >. e. NrmCVec <-> ( <. G , S >. e. CVecOLD /\ N : X --> RR /\ A. x e. X ( ( ( N ` x ) = 0 -> x = ( GId ` G ) ) /\ A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) )
16 12 15 sylib 
 |-  ( U e. NrmCVec -> ( <. G , S >. e. CVecOLD /\ N : X --> RR /\ A. x e. X ( ( ( N ` x ) = 0 -> x = ( GId ` G ) ) /\ A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) )
17 2 4 0vfval 
 |-  ( U e. NrmCVec -> Z = ( GId ` G ) )
18 17 eqeq2d 
 |-  ( U e. NrmCVec -> ( x = Z <-> x = ( GId ` G ) ) )
19 18 imbi2d 
 |-  ( U e. NrmCVec -> ( ( ( N ` x ) = 0 -> x = Z ) <-> ( ( N ` x ) = 0 -> x = ( GId ` G ) ) ) )
20 19 3anbi1d 
 |-  ( U e. NrmCVec -> ( ( ( ( N ` x ) = 0 -> x = Z ) /\ A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) <-> ( ( ( N ` x ) = 0 -> x = ( GId ` G ) ) /\ A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) )
21 20 ralbidv 
 |-  ( U e. NrmCVec -> ( A. x e. X ( ( ( N ` x ) = 0 -> x = Z ) /\ A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) <-> A. x e. X ( ( ( N ` x ) = 0 -> x = ( GId ` G ) ) /\ A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) )
22 21 3anbi3d 
 |-  ( U e. NrmCVec -> ( ( <. G , S >. e. CVecOLD /\ N : X --> RR /\ A. x e. X ( ( ( N ` x ) = 0 -> x = Z ) /\ A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) <-> ( <. G , S >. e. CVecOLD /\ N : X --> RR /\ A. x e. X ( ( ( N ` x ) = 0 -> x = ( GId ` G ) ) /\ A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) ) )
23 16 22 mpbird 
 |-  ( U e. NrmCVec -> ( <. G , S >. e. CVecOLD /\ N : X --> RR /\ A. x e. X ( ( ( N ` x ) = 0 -> x = Z ) /\ A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) )