Theorem hlnv

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

	Ref	Expression
Assertion	hlnv	$$⊢U\in {CHil}_{\mathrm{OLD}}\to U\in \mathrm{NrmCVec}$$

Proof

Step	Hyp	Ref	Expression
1		hlobn	$$⊢U\in {CHil}_{\mathrm{OLD}}\to U\in \mathrm{CBan}$$
2		bnnv	$$⊢U\in \mathrm{CBan}\to U\in \mathrm{NrmCVec}$$
3	1 2	syl	$$⊢U\in {CHil}_{\mathrm{OLD}}\to U\in \mathrm{NrmCVec}$$