This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isnvi

Description: Properties that determine a normed complex vector space. (Contributed by NM, 15-Apr-2007) (New usage is discouraged.)

Ref Expression
Hypotheses isnvi.5 
|- X = ran G
isnvi.6 
|- Z = ( GId ` G )
isnvi.7 
|- <. G , S >. e. CVecOLD
isnvi.8 
|- N : X --> RR
isnvi.9 
|- ( ( x e. X /\ ( N ` x ) = 0 ) -> x = Z )
isnvi.10 
|- ( ( y e. CC /\ x e. X ) -> ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) )
isnvi.11 
|- ( ( x e. X /\ y e. X ) -> ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) )
isnvi.12 
|- U = <. <. G , S >. , N >.
Assertion isnvi 
|- U e. NrmCVec

Proof

Step Hyp Ref Expression
1 isnvi.5 
 |-  X = ran G
2 isnvi.6 
 |-  Z = ( GId ` G )
3 isnvi.7 
 |-  <. G , S >. e. CVecOLD
4 isnvi.8 
 |-  N : X --> RR
5 isnvi.9 
 |-  ( ( x e. X /\ ( N ` x ) = 0 ) -> x = Z )
6 isnvi.10 
 |-  ( ( y e. CC /\ x e. X ) -> ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) )
7 isnvi.11 
 |-  ( ( x e. X /\ y e. X ) -> ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) )
8 isnvi.12 
 |-  U = <. <. G , S >. , N >.
9 5 ex 
 |-  ( x e. X -> ( ( N ` x ) = 0 -> x = Z ) )
10 6 ancoms 
 |-  ( ( x e. X /\ y e. CC ) -> ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) )
11 10 ralrimiva 
 |-  ( x e. X -> A. y e. CC ( N ` ( y S x ) ) = ( ( abs ` y ) x. ( N ` x ) ) )
12 7 ralrimiva 
 |-  ( x e. X -> A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) )
13 9 11 12 3jca 
 |-  ( 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 ) ) ) )
14 13 rgen 
 |-  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 ) ) )
15 1 2 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 ) ) ) ) )
16 3 4 14 15 mpbir3an 
 |-  <. <. G , S >. , N >. e. NrmCVec
17 8 16 eqeltri 
 |-  U e. NrmCVec