This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdmda ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )