Theorem phnvi

Description: Every complex inner product space is a normed complex vector space. (Contributed by NM, 20-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypothesis	phnvi.1	⊢ 𝑈 ∈ CPreHilOLD
Assertion	phnvi	⊢ 𝑈 ∈ NrmCVec

Proof

Step	Hyp	Ref	Expression
1		phnvi.1	⊢ 𝑈 ∈ CPreHilOLD
2		phnv	⊢ ( 𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec )
3	1 2	ax-mp	⊢ 𝑈 ∈ NrmCVec