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