Theorem nvcl

Description: The norm of a normed complex vector space is a real number. (Contributed by NM, 24-Nov-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvf.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	nvf.6	⊢ 𝑁 = ( normCV ‘ 𝑈 )
Assertion	nvcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		nvf.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		nvf.6	⊢ 𝑁 = ( normCV ‘ 𝑈 )
3	1 2	nvf	⊢ ( 𝑈 ∈ NrmCVec → 𝑁 : 𝑋 ⟶ ℝ )
4	3	ffvelrnda	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )