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	⊢ ( 𝑈 ∈ CHilOLD → 𝑈 ∈ NrmCVec )

Proof

Step	Hyp	Ref	Expression
1		hlobn	⊢ ( 𝑈 ∈ CHilOLD → 𝑈 ∈ CBan )
2		bnnv	⊢ ( 𝑈 ∈ CBan → 𝑈 ∈ NrmCVec )
3	1 2	syl	⊢ ( 𝑈 ∈ CHilOLD → 𝑈 ∈ NrmCVec )