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	⊢ 𝑈 ∈ CHilOLD
Assertion	hlnvi	⊢ 𝑈 ∈ NrmCVec

Proof

Step	Hyp	Ref	Expression
1		hlnvi.1	⊢ 𝑈 ∈ CHilOLD
2		hlnv	⊢ ( 𝑈 ∈ CHilOLD → 𝑈 ∈ NrmCVec )
3	1 2	ax-mp	⊢ 𝑈 ∈ NrmCVec