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

Metamath Proof Explorer

Theorem cnnv

Description: The set of complex numbers is a normed complex vector space. The vector operation is + , the scalar product is x. , and the norm function is abs . (Contributed by Steve Rodriguez, 3-Dec-2006) (New usage is discouraged.)

Ref Expression
Hypothesis cnnv.6 
|- U = <. <. + , x. >. , abs >.
Assertion cnnv 
|- U e. NrmCVec

Proof

Step Hyp Ref Expression
1 cnnv.6 
 |-  U = <. <. + , x. >. , abs >.
2 cnaddabloOLD 
 |-  + e. AbelOp
3 ablogrpo 
 |-  ( + e. AbelOp -> + e. GrpOp )
4 2 3 ax-mp 
 |-  + e. GrpOp
5 ax-addf 
 |-  + : ( CC X. CC ) --> CC
6 5 fdmi 
 |-  dom + = ( CC X. CC )
7 4 6 grporn 
 |-  CC = ran +
8 cnidOLD 
 |-  0 = ( GId ` + )
9 cncvcOLD 
 |-  <. + , x. >. e. CVecOLD
10 absf 
 |-  abs : CC --> RR
11 abs00 
 |-  ( x e. CC -> ( ( abs ` x ) = 0 <-> x = 0 ) )
12 11 biimpa 
 |-  ( ( x e. CC /\ ( abs ` x ) = 0 ) -> x = 0 )
13 absmul 
 |-  ( ( y e. CC /\ x e. CC ) -> ( abs ` ( y x. x ) ) = ( ( abs ` y ) x. ( abs ` x ) ) )
14 abstri 
 |-  ( ( x e. CC /\ y e. CC ) -> ( abs ` ( x + y ) ) <_ ( ( abs ` x ) + ( abs ` y ) ) )
15 7 8 9 10 12 13 14 1 isnvi 
 |-  U e. NrmCVec