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	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
	nvf.6	$$⊢N={norm}_{CV}\left(U\right)$$
Assertion	nvcl	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\right)\to N\left(A\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		nvf.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		nvf.6	$$⊢N={norm}_{CV}\left(U\right)$$
3	1 2	nvf	$$⊢U\in \mathrm{NrmCVec}\to N:X⟶ℝ$$
4	3	ffvelrnda	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\right)\to N\left(A\right)\in ℝ$$