Theorem nvcli

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

	Ref	Expression
Hypotheses	nvf.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	nvf.6	⊢ 𝑁 = ( normCV ‘ 𝑈 )
	nvcli.9	⊢ 𝑈 ∈ NrmCVec
	nvcli.7	⊢ 𝐴 ∈ 𝑋
Assertion	nvcli	⊢ ( 𝑁 ‘ 𝐴 ) ∈ ℝ

Proof

Step	Hyp	Ref	Expression
1		nvf.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		nvf.6	⊢ 𝑁 = ( normCV ‘ 𝑈 )
3		nvcli.9	⊢ 𝑈 ∈ NrmCVec
4		nvcli.7	⊢ 𝐴 ∈ 𝑋
5	1 2	nvcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )
6	3 4 5	mp2an	⊢ ( 𝑁 ‘ 𝐴 ) ∈ ℝ