Theorem hhnv

Description: Hilbert space is a normed complex vector space. (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hhnv.1	|- U = <. <. +h , .h >. , normh >.
Assertion	hhnv	|- U e. NrmCVec

Proof

Step	Hyp	Ref	Expression
1		hhnv.1	|- U = <. <. +h , .h >. , normh >.
2		hilablo	|- +h e. AbelOp
3		ablogrpo	|- ( +h e. AbelOp -> +h e. GrpOp )
4	2 3	ax-mp	|- +h e. GrpOp
5		ax-hfvadd	|- +h : ( ~H X. ~H ) --> ~H
6	5	fdmi	|- dom +h = ( ~H X. ~H )
7	4 6	grporn	|- ~H = ran +h
8		hilid	|- ( GId ` +h ) = 0h
9	8	eqcomi	|- 0h = ( GId ` +h )
10		hilvc	|- <. +h , .h >. e. CVecOLD
11		normf	|- normh : ~H --> RR
12		norm-i	|- ( x e. ~H -> ( ( normh ` x ) = 0 <-> x = 0h ) )
13	12	biimpa	|- ( ( x e. ~H /\ ( normh ` x ) = 0 ) -> x = 0h )
14		norm-iii	|- ( ( y e. CC /\ x e. ~H ) -> ( normh ` ( y .h x ) ) = ( ( abs ` y ) x. ( normh ` x ) ) )
15		norm-ii	|- ( ( x e. ~H /\ y e. ~H ) -> ( normh ` ( x +h y ) ) <_ ( ( normh ` x ) + ( normh ` y ) ) )
16	7 9 10 11 13 14 15 1	isnvi	|- U e. NrmCVec