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