Theorem nmcnc

Description: The norm of a normed complex vector space is a continuous function to CC . (For RR , see nmcvcn .) (Contributed by NM, 12-Aug-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nmcnc.1	$$⊢N={norm}_{CV}\left(U\right)$$
	nmcnc.2	$$⊢C=\mathrm{IndMet}\left(U\right)$$
	nmcnc.j	$$⊢J=\mathrm{MetOpen}\left(C\right)$$
	nmcnc.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	nmcnc	$$⊢U\in \mathrm{NrmCVec}\to N\in \left(J\mathrm{Cn}K\right)$$

Proof

Step	Hyp	Ref	Expression
1		nmcnc.1	$$⊢N={norm}_{CV}\left(U\right)$$
2		nmcnc.2	$$⊢C=\mathrm{IndMet}\left(U\right)$$
3		nmcnc.j	$$⊢J=\mathrm{MetOpen}\left(C\right)$$
4		nmcnc.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
5	4	cnfldtop	$$⊢K\in \mathrm{Top}$$
6		cnrest2r	$$⊢K\in \mathrm{Top}\to J\mathrm{Cn}\left(K{\upharpoonright }_{𝑡}ℝ\right)\subseteq J\mathrm{Cn}K$$
7	5 6	ax-mp	$$⊢J\mathrm{Cn}\left(K{\upharpoonright }_{𝑡}ℝ\right)\subseteq J\mathrm{Cn}K$$
8	4	tgioo2	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=K{\upharpoonright }_{𝑡}ℝ$$
9	8	eqcomi	$$⊢K{\upharpoonright }_{𝑡}ℝ=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
10	1 2 3 9	nmcvcn	$$⊢U\in \mathrm{NrmCVec}\to N\in \left(J\mathrm{Cn}\left(K{\upharpoonright }_{𝑡}ℝ\right)\right)$$
11	7 10	sseldi	$$⊢U\in \mathrm{NrmCVec}\to N\in \left(J\mathrm{Cn}K\right)$$