Theorem rrhcn

Description: If the topology of R is Hausdorff, and R is a complete uniform space, then the canonical homomorphism from the real numbers to R is continuous. (Contributed by Thierry Arnoux, 17-Jan-2018)

	Ref	Expression
Hypotheses	rrhf.d	$$⊢D={\mathrm{dist}\left(R\right)\upharpoonright }_{\left(B\times B\right)}$$
	rrhf.j	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
	rrhf.b	$$⊢B={\mathrm{Base}}_R$$
	rrhf.k	$$⊢K=\mathrm{TopOpen}\left(R\right)$$
	rrhf.z	$$⊢Z=\mathrm{\mathbb{Z}Mod}\left(R\right)$$
	rrhf.1	$$⊢\phi \to R\in \mathrm{DivRing}$$
	rrhf.2	$$⊢\phi \to R\in \mathrm{NrmRing}$$
	rrhf.3	$$⊢\phi \to Z\in \mathrm{NrmMod}$$
	rrhf.4	$$⊢\phi \to \mathrm{chr}\left(R\right)=0$$
	rrhf.5	$$⊢\phi \to R\in \mathrm{CUnifSp}$$
	rrhf.6	$$⊢\phi \to \mathrm{UnifSt}\left(R\right)=\mathrm{metUnif}\left(D\right)$$
Assertion	rrhcn	$$⊢\phi \to \mathrm{ℝHom}\left(R\right)\in \left(J\mathrm{Cn}K\right)$$

Proof

Step	Hyp	Ref	Expression
1		rrhf.d	$$⊢D={\mathrm{dist}\left(R\right)\upharpoonright }_{\left(B\times B\right)}$$
2		rrhf.j	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
3		rrhf.b	$$⊢B={\mathrm{Base}}_R$$
4		rrhf.k	$$⊢K=\mathrm{TopOpen}\left(R\right)$$
5		rrhf.z	$$⊢Z=\mathrm{\mathbb{Z}Mod}\left(R\right)$$
6		rrhf.1	$$⊢\phi \to R\in \mathrm{DivRing}$$
7		rrhf.2	$$⊢\phi \to R\in \mathrm{NrmRing}$$
8		rrhf.3	$$⊢\phi \to Z\in \mathrm{NrmMod}$$
9		rrhf.4	$$⊢\phi \to \mathrm{chr}\left(R\right)=0$$
10		rrhf.5	$$⊢\phi \to R\in \mathrm{CUnifSp}$$
11		rrhf.6	$$⊢\phi \to \mathrm{UnifSt}\left(R\right)=\mathrm{metUnif}\left(D\right)$$
12		nrgngp	$$⊢R\in \mathrm{NrmRing}\to R\in \mathrm{NrmGrp}$$
13		ngpxms	$$⊢R\in \mathrm{NrmGrp}\to R\in \mathrm{\infty MetSp}$$
14	7 12 13	3syl	$$⊢\phi \to R\in \mathrm{\infty MetSp}$$
15		xmstps	$$⊢R\in \mathrm{\infty MetSp}\to R\in \mathrm{TopSp}$$
16	14 15	syl	$$⊢\phi \to R\in \mathrm{TopSp}$$
17	2 4	rrhval	$$⊢R\in \mathrm{TopSp}\to \mathrm{ℝHom}\left(R\right)=\left(J\mathrm{CnExt}K\right)\left(\mathrm{\mathbb{Q}Hom}\left(R\right)\right)$$
18	16 17	syl	$$⊢\phi \to \mathrm{ℝHom}\left(R\right)=\left(J\mathrm{CnExt}K\right)\left(\mathrm{\mathbb{Q}Hom}\left(R\right)\right)$$
19		rebase	$$⊢ℝ={\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$$
20		retopn	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℝ}_{\mathrm{fld}}\right)$$
21	2 20	eqtri	$$⊢J=\mathrm{TopOpen}\left({ℝ}_{\mathrm{fld}}\right)$$
22		eqid	$$⊢\mathrm{UnifSt}\left({ℝ}_{\mathrm{fld}}\right)=\mathrm{UnifSt}\left({ℝ}_{\mathrm{fld}}\right)$$
23		df-refld	$$⊢{ℝ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ$$
24	23	oveq1i	$$⊢{ℝ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}=\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right){\upharpoonright }_{𝑠}\mathbb{Q}$$
25		reex	$$⊢ℝ\in \mathrm{V}$$
26		qssre	$$⊢\mathbb{Q}\subseteq ℝ$$
27		ressabs	$$⊢\left(ℝ\in \mathrm{V}\wedge \mathbb{Q}\subseteq ℝ\right)\to \left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right){\upharpoonright }_{𝑠}\mathbb{Q}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
28	25 26 27	mp2an	$$⊢\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\right){\upharpoonright }_{𝑠}\mathbb{Q}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
29	24 28	eqtr2i	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}={ℝ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
30	29	fveq2i	$$⊢\mathrm{UnifSt}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)=\mathrm{UnifSt}\left({ℝ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)$$
31		eqid	$$⊢\mathrm{UnifSt}\left(R\right)=\mathrm{UnifSt}\left(R\right)$$
32		recms	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{CMetSp}$$
33		cmsms	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{CMetSp}\to {ℝ}_{\mathrm{fld}}\in \mathrm{MetSp}$$
34		mstps	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{MetSp}\to {ℝ}_{\mathrm{fld}}\in \mathrm{TopSp}$$
35	32 33 34	mp2b	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{TopSp}$$
36	35	a1i	$$⊢\phi \to {ℝ}_{\mathrm{fld}}\in \mathrm{TopSp}$$
37		recusp	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{CUnifSp}$$
38		cuspusp	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{CUnifSp}\to {ℝ}_{\mathrm{fld}}\in \mathrm{UnifSp}$$
39	37 38	mp1i	$$⊢\phi \to {ℝ}_{\mathrm{fld}}\in \mathrm{UnifSp}$$
40	4 3 1	xmstopn	$$⊢R\in \mathrm{\infty MetSp}\to K=\mathrm{MetOpen}\left(D\right)$$
41	14 40	syl	$$⊢\phi \to K=\mathrm{MetOpen}\left(D\right)$$
42	3 1	xmsxmet	$$⊢R\in \mathrm{\infty MetSp}\to D\in \mathrm{\infty Met}\left(B\right)$$
43		eqid	$$⊢\mathrm{MetOpen}\left(D\right)=\mathrm{MetOpen}\left(D\right)$$
44	43	methaus	$$⊢D\in \mathrm{\infty Met}\left(B\right)\to \mathrm{MetOpen}\left(D\right)\in \mathrm{Haus}$$
45	14 42 44	3syl	$$⊢\phi \to \mathrm{MetOpen}\left(D\right)\in \mathrm{Haus}$$
46	41 45	eqeltrd	$$⊢\phi \to K\in \mathrm{Haus}$$
47	26	a1i	$$⊢\phi \to \mathbb{Q}\subseteq ℝ$$
48		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
49		eqid	$$⊢\mathrm{UnifSt}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)=\mathrm{UnifSt}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)$$
50	1	fveq2i	$$⊢\mathrm{metUnif}\left(D\right)=\mathrm{metUnif}\left({\mathrm{dist}\left(R\right)\upharpoonright }_{\left(B\times B\right)}\right)$$
51	3 48 49 50 5 7 6 8 9	qqhucn	$$⊢\phi \to \mathrm{\mathbb{Q}Hom}\left(R\right)\in \left(\mathrm{UnifSt}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\mathrm{uCn}\mathrm{metUnif}\left(D\right)\right)$$
52	11	eqcomd	$$⊢\phi \to \mathrm{metUnif}\left(D\right)=\mathrm{UnifSt}\left(R\right)$$
53	52	oveq2d	$$⊢\phi \to \mathrm{UnifSt}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\mathrm{uCn}\mathrm{metUnif}\left(D\right)=\mathrm{UnifSt}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\mathrm{uCn}\mathrm{UnifSt}\left(R\right)$$
54	51 53	eleqtrd	$$⊢\phi \to \mathrm{\mathbb{Q}Hom}\left(R\right)\in \left(\mathrm{UnifSt}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\mathrm{uCn}\mathrm{UnifSt}\left(R\right)\right)$$
55	2	fveq2i	$$⊢\mathrm{cls}\left(J\right)=\mathrm{cls}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
56	55	fveq1i	$$⊢\mathrm{cls}\left(J\right)\left(\mathbb{Q}\right)=\mathrm{cls}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\mathbb{Q}\right)$$
57		qdensere	$$⊢\mathrm{cls}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\mathbb{Q}\right)=ℝ$$
58	56 57	eqtri	$$⊢\mathrm{cls}\left(J\right)\left(\mathbb{Q}\right)=ℝ$$
59	58	a1i	$$⊢\phi \to \mathrm{cls}\left(J\right)\left(\mathbb{Q}\right)=ℝ$$
60	19 3 21 4 22 30 31 36 39 16 10 46 47 54 59	ucnextcn	$$⊢\phi \to \left(J\mathrm{CnExt}K\right)\left(\mathrm{\mathbb{Q}Hom}\left(R\right)\right)\in \left(J\mathrm{Cn}K\right)$$
61	18 60	eqeltrd	$$⊢\phi \to \mathrm{ℝHom}\left(R\right)\in \left(J\mathrm{Cn}K\right)$$