Theorem ngnmcncn

Description: The norm of a normed group is a continuous function to CC . (Contributed by NM, 12-Aug-2007) (Revised by AV, 17-Oct-2021)

	Ref	Expression
Hypotheses	nmcn.n	$$⊢N=\mathrm{norm}\left(G\right)$$
	nmcn.j	$$⊢J=\mathrm{TopOpen}\left(G\right)$$
	ngnmcncn.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	ngnmcncn	$$⊢G\in \mathrm{NrmGrp}\to N\in \left(J\mathrm{Cn}K\right)$$

Proof

Step	Hyp	Ref	Expression
1		nmcn.n	$$⊢N=\mathrm{norm}\left(G\right)$$
2		nmcn.j	$$⊢J=\mathrm{TopOpen}\left(G\right)$$
3		ngnmcncn.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
4	3	cnfldtop	$$⊢K\in \mathrm{Top}$$
5		cnrest2r	$$⊢K\in \mathrm{Top}\to J\mathrm{Cn}\left(K{\upharpoonright }_{𝑡}ℝ\right)\subseteq J\mathrm{Cn}K$$
6	4 5	ax-mp	$$⊢J\mathrm{Cn}\left(K{\upharpoonright }_{𝑡}ℝ\right)\subseteq J\mathrm{Cn}K$$
7	3	tgioo2	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=K{\upharpoonright }_{𝑡}ℝ$$
8	7	eqcomi	$$⊢K{\upharpoonright }_{𝑡}ℝ=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
9	1 2 8	nmcn	$$⊢G\in \mathrm{NrmGrp}\to N\in \left(J\mathrm{Cn}\left(K{\upharpoonright }_{𝑡}ℝ\right)\right)$$
10	6 9	sseldi	$$⊢G\in \mathrm{NrmGrp}\to N\in \left(J\mathrm{Cn}K\right)$$