Metamath Proof Explorer

Theorem isnv

Description: The predicate "is a normed complex vector space." (Contributed by NM, 5-Jun-2008) (New usage is discouraged.)

Ref Expression
Hypotheses isnv.1 
|- X = ran G
isnv.2 
|- Z = ( GId ` G )
Assertion isnv 
|- ( <. <. G , S >. , N >. 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 isnv.1 
 |-  X = ran G
2 isnv.2 
 |-  Z = ( GId ` G )
3 nvex 
 |-  ( <. <. G , S >. , N >. e. NrmCVec -> ( G e. _V /\ S e. _V /\ N e. _V ) )
4 vcex 
 |-  ( <. G , S >. e. CVecOLD -> ( G e. _V /\ S e. _V ) )
5 4 adantr 
 |-  ( ( <. G , S >. e. CVecOLD /\ N : X --> RR ) -> ( G e. _V /\ S e. _V ) )
6 4 simpld 
 |-  ( <. G , S >. e. CVecOLD -> G e. _V )
7 rnexg 
 |-  ( G e. _V -> ran G e. _V )
8 6 7 syl 
 |-  ( <. G , S >. e. CVecOLD -> ran G e. _V )
9 1 8 eqeltrid 
 |-  ( <. G , S >. e. CVecOLD -> X e. _V )
10 fex 
 |-  ( ( N : X --> RR /\ X e. _V ) -> N e. _V )
11 9 10 sylan2 
 |-  ( ( N : X --> RR /\ <. G , S >. e. CVecOLD ) -> N e. _V )
12 11 ancoms 
 |-  ( ( <. G , S >. e. CVecOLD /\ N : X --> RR ) -> N e. _V )
13 df-3an 
 |-  ( ( G e. _V /\ S e. _V /\ N e. _V ) <-> ( ( G e. _V /\ S e. _V ) /\ N e. _V ) )
14 5 12 13 sylanbrc 
 |-  ( ( <. G , S >. e. CVecOLD /\ N : X --> RR ) -> ( G e. _V /\ S e. _V /\ N e. _V ) )
15 14 3adant3 
 |-  ( ( <. 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 e. _V /\ S e. _V /\ N e. _V ) )
16 1 2 isnvlem 
 |-  ( ( G e. _V /\ S e. _V /\ N e. _V ) -> ( <. <. G , S >. , N >. 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 ) ) ) ) ) )
17 3 15 16 pm5.21nii 
 |-  ( <. <. G , S >. , N >. 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 ) ) ) ) )