Theorem rrhcne

Description: If R is an extension of RR , then the canonical homomorphism of RR into R is continuous. (Contributed by Thierry Arnoux, 2-May-2018)

	Ref	Expression
Hypotheses	rrhcne.j	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
	rrhcne.k	$$⊢K=\mathrm{TopOpen}\left(R\right)$$
Assertion	rrhcne	$$⊢R\in \mathrm{ℝExt}\to \mathrm{ℝHom}\left(R\right)\in \left(J\mathrm{Cn}K\right)$$

Proof

Step	Hyp	Ref	Expression
1		rrhcne.j	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
2		rrhcne.k	$$⊢K=\mathrm{TopOpen}\left(R\right)$$
3		eqid	$$⊢{\mathrm{dist}\left(R\right)\upharpoonright }_{\left({\mathrm{Base}}_R\times {\mathrm{Base}}_R\right)}={\mathrm{dist}\left(R\right)\upharpoonright }_{\left({\mathrm{Base}}_R\times {\mathrm{Base}}_R\right)}$$
4		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
5		eqid	$$⊢\mathrm{\mathbb{Z}Mod}\left(R\right)=\mathrm{\mathbb{Z}Mod}\left(R\right)$$
6		rrextdrg	$$⊢R\in \mathrm{ℝExt}\to R\in \mathrm{DivRing}$$
7		rrextnrg	$$⊢R\in \mathrm{ℝExt}\to R\in \mathrm{NrmRing}$$
8	5	rrextnlm	$$⊢R\in \mathrm{ℝExt}\to \mathrm{\mathbb{Z}Mod}\left(R\right)\in \mathrm{NrmMod}$$
9		rrextchr	$$⊢R\in \mathrm{ℝExt}\to \mathrm{chr}\left(R\right)=0$$
10		rrextcusp	$$⊢R\in \mathrm{ℝExt}\to R\in \mathrm{CUnifSp}$$
11	4 3	rrextust	$$⊢R\in \mathrm{ℝExt}\to \mathrm{UnifSt}\left(R\right)=\mathrm{metUnif}\left({\mathrm{dist}\left(R\right)\upharpoonright }_{\left({\mathrm{Base}}_R\times {\mathrm{Base}}_R\right)}\right)$$
12	3 1 4 2 5 6 7 8 9 10 11	rrhcn	$$⊢R\in \mathrm{ℝExt}\to \mathrm{ℝHom}\left(R\right)\in \left(J\mathrm{Cn}K\right)$$