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