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