Theorem hlnvi

Description: Every complex Hilbert space is a normed complex vector space. (Contributed by NM, 6-Jun-2008) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hlnvi.1	|- U e. CHilOLD
Assertion	hlnvi	|- U e. NrmCVec

Proof

Step	Hyp	Ref	Expression
1		hlnvi.1	|- U e. CHilOLD
2		hlnv	|- ( U e. CHilOLD -> U e. NrmCVec )
3	1 2	ax-mp	|- U e. NrmCVec