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\in {CHil}_{\mathrm{OLD}}$$
Assertion	hlnvi	$$⊢U\in \mathrm{NrmCVec}$$

Proof

Step	Hyp	Ref	Expression
1		hlnvi.1	$$⊢U\in {CHil}_{\mathrm{OLD}}$$
2		hlnv	$$⊢U\in {CHil}_{\mathrm{OLD}}\to U\in \mathrm{NrmCVec}$$
3	1 2	ax-mp	$$⊢U\in \mathrm{NrmCVec}$$