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	⊢ 𝐷 = ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) )
	rrhf.j	⊢ 𝐽 = ( topGen ‘ ran (,) )
	rrhf.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rrhf.k	⊢ 𝐾 = ( TopOpen ‘ 𝑅 )
	rrhf.z	⊢ 𝑍 = ( ℤMod ‘ 𝑅 )
	rrhf.1	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
	rrhf.2	⊢ ( 𝜑 → 𝑅 ∈ NrmRing )
	rrhf.3	⊢ ( 𝜑 → 𝑍 ∈ NrmMod )
	rrhf.4	⊢ ( 𝜑 → ( chr ‘ 𝑅 ) = 0 )
	rrhf.5	⊢ ( 𝜑 → 𝑅 ∈ CUnifSp )
	rrhf.6	⊢ ( 𝜑 → ( UnifSt ‘ 𝑅 ) = ( metUnif ‘ 𝐷 ) )
Assertion	rrhcn	⊢ ( 𝜑 → ( ℝHom ‘ 𝑅 ) ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		rrhf.d	⊢ 𝐷 = ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) )
2		rrhf.j	⊢ 𝐽 = ( topGen ‘ ran (,) )
3		rrhf.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		rrhf.k	⊢ 𝐾 = ( TopOpen ‘ 𝑅 )
5		rrhf.z	⊢ 𝑍 = ( ℤMod ‘ 𝑅 )
6		rrhf.1	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
7		rrhf.2	⊢ ( 𝜑 → 𝑅 ∈ NrmRing )
8		rrhf.3	⊢ ( 𝜑 → 𝑍 ∈ NrmMod )
9		rrhf.4	⊢ ( 𝜑 → ( chr ‘ 𝑅 ) = 0 )
10		rrhf.5	⊢ ( 𝜑 → 𝑅 ∈ CUnifSp )
11		rrhf.6	⊢ ( 𝜑 → ( UnifSt ‘ 𝑅 ) = ( metUnif ‘ 𝐷 ) )
12		nrgngp	⊢ ( 𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp )
13		ngpxms	⊢ ( 𝑅 ∈ NrmGrp → 𝑅 ∈ ∞MetSp )
14	7 12 13	3syl	⊢ ( 𝜑 → 𝑅 ∈ ∞MetSp )
15		xmstps	⊢ ( 𝑅 ∈ ∞MetSp → 𝑅 ∈ TopSp )
16	14 15	syl	⊢ ( 𝜑 → 𝑅 ∈ TopSp )
17	2 4	rrhval	⊢ ( 𝑅 ∈ TopSp → ( ℝHom ‘ 𝑅 ) = ( ( 𝐽 CnExt 𝐾 ) ‘ ( ℚHom ‘ 𝑅 ) ) )
18	16 17	syl	⊢ ( 𝜑 → ( ℝHom ‘ 𝑅 ) = ( ( 𝐽 CnExt 𝐾 ) ‘ ( ℚHom ‘ 𝑅 ) ) )
19		rebase	⊢ ℝ = ( Base ‘ ℝfld )
20		retopn	⊢ ( topGen ‘ ran (,) ) = ( TopOpen ‘ ℝfld )
21	2 20	eqtri	⊢ 𝐽 = ( TopOpen ‘ ℝfld )
22		eqid	⊢ ( UnifSt ‘ ℝfld ) = ( UnifSt ‘ ℝfld )
23		df-refld	⊢ ℝfld = ( ℂfld ↾s ℝ )
24	23	oveq1i	⊢ ( ℝfld ↾s ℚ ) = ( ( ℂfld ↾s ℝ ) ↾s ℚ )
25		reex	⊢ ℝ ∈ V
26		qssre	⊢ ℚ ⊆ ℝ
27		ressabs	⊢ ( ( ℝ ∈ V ∧ ℚ ⊆ ℝ ) → ( ( ℂfld ↾s ℝ ) ↾s ℚ ) = ( ℂfld ↾s ℚ ) )
28	25 26 27	mp2an	⊢ ( ( ℂfld ↾s ℝ ) ↾s ℚ ) = ( ℂfld ↾s ℚ )
29	24 28	eqtr2i	⊢ ( ℂfld ↾s ℚ ) = ( ℝfld ↾s ℚ )
30	29	fveq2i	⊢ ( UnifSt ‘ ( ℂfld ↾s ℚ ) ) = ( UnifSt ‘ ( ℝfld ↾s ℚ ) )
31		eqid	⊢ ( UnifSt ‘ 𝑅 ) = ( UnifSt ‘ 𝑅 )
32		recms	⊢ ℝfld ∈ CMetSp
33		cmsms	⊢ ( ℝfld ∈ CMetSp → ℝfld ∈ MetSp )
34		mstps	⊢ ( ℝfld ∈ MetSp → ℝfld ∈ TopSp )
35	32 33 34	mp2b	⊢ ℝfld ∈ TopSp
36	35	a1i	⊢ ( 𝜑 → ℝfld ∈ TopSp )
37		recusp	⊢ ℝfld ∈ CUnifSp
38		cuspusp	⊢ ( ℝfld ∈ CUnifSp → ℝfld ∈ UnifSp )
39	37 38	mp1i	⊢ ( 𝜑 → ℝfld ∈ UnifSp )
40	4 3 1	xmstopn	⊢ ( 𝑅 ∈ ∞MetSp → 𝐾 = ( MetOpen ‘ 𝐷 ) )
41	14 40	syl	⊢ ( 𝜑 → 𝐾 = ( MetOpen ‘ 𝐷 ) )
42	3 1	xmsxmet	⊢ ( 𝑅 ∈ ∞MetSp → 𝐷 ∈ ( ∞Met ‘ 𝐵 ) )
43		eqid	⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 )
44	43	methaus	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) → ( MetOpen ‘ 𝐷 ) ∈ Haus )
45	14 42 44	3syl	⊢ ( 𝜑 → ( MetOpen ‘ 𝐷 ) ∈ Haus )
46	41 45	eqeltrd	⊢ ( 𝜑 → 𝐾 ∈ Haus )
47	26	a1i	⊢ ( 𝜑 → ℚ ⊆ ℝ )
48		eqid	⊢ ( ℂfld ↾s ℚ ) = ( ℂfld ↾s ℚ )
49		eqid	⊢ ( UnifSt ‘ ( ℂfld ↾s ℚ ) ) = ( UnifSt ‘ ( ℂfld ↾s ℚ ) )
50	1	fveq2i	⊢ ( metUnif ‘ 𝐷 ) = ( metUnif ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) )
51	3 48 49 50 5 7 6 8 9	qqhucn	⊢ ( 𝜑 → ( ℚHom ‘ 𝑅 ) ∈ ( ( UnifSt ‘ ( ℂfld ↾s ℚ ) ) Cnu ( metUnif ‘ 𝐷 ) ) )
52	11	eqcomd	⊢ ( 𝜑 → ( metUnif ‘ 𝐷 ) = ( UnifSt ‘ 𝑅 ) )
53	52	oveq2d	⊢ ( 𝜑 → ( ( UnifSt ‘ ( ℂfld ↾s ℚ ) ) Cnu ( metUnif ‘ 𝐷 ) ) = ( ( UnifSt ‘ ( ℂfld ↾s ℚ ) ) Cnu ( UnifSt ‘ 𝑅 ) ) )
54	51 53	eleqtrd	⊢ ( 𝜑 → ( ℚHom ‘ 𝑅 ) ∈ ( ( UnifSt ‘ ( ℂfld ↾s ℚ ) ) Cnu ( UnifSt ‘ 𝑅 ) ) )
55	2	fveq2i	⊢ ( cls ‘ 𝐽 ) = ( cls ‘ ( topGen ‘ ran (,) ) )
56	55	fveq1i	⊢ ( ( cls ‘ 𝐽 ) ‘ ℚ ) = ( ( cls ‘ ( topGen ‘ ran (,) ) ) ‘ ℚ )
57		qdensere	⊢ ( ( cls ‘ ( topGen ‘ ran (,) ) ) ‘ ℚ ) = ℝ
58	56 57	eqtri	⊢ ( ( cls ‘ 𝐽 ) ‘ ℚ ) = ℝ
59	58	a1i	⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ ℚ ) = ℝ )
60	19 3 21 4 22 30 31 36 39 16 10 46 47 54 59	ucnextcn	⊢ ( 𝜑 → ( ( 𝐽 CnExt 𝐾 ) ‘ ( ℚHom ‘ 𝑅 ) ) ∈ ( 𝐽 Cn 𝐾 ) )
61	18 60	eqeltrd	⊢ ( 𝜑 → ( ℝHom ‘ 𝑅 ) ∈ ( 𝐽 Cn 𝐾 ) )