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 = ( ( dist ` R ) \|` ( B X. B ) )
	rrhf.j	\|- J = ( topGen ` ran (,) )
	rrhf.b	\|- B = ( Base ` R )
	rrhf.k	\|- K = ( TopOpen ` R )
	rrhf.z	\|- Z = ( ZMod ` R )
	rrhf.1	\|- ( ph -> R e. DivRing )
	rrhf.2	\|- ( ph -> R e. NrmRing )
	rrhf.3	\|- ( ph -> Z e. NrmMod )
	rrhf.4	\|- ( ph -> ( chr ` R ) = 0 )
	rrhf.5	\|- ( ph -> R e. CUnifSp )
	rrhf.6	\|- ( ph -> ( UnifSt ` R ) = ( metUnif ` D ) )
Assertion	rrhcn	\|- ( ph -> ( RRHom ` R ) e. ( J Cn K ) )

Proof

Step	Hyp	Ref	Expression
1		rrhf.d	\|- D = ( ( dist ` R ) \|` ( B X. B ) )
2		rrhf.j	\|- J = ( topGen ` ran (,) )
3		rrhf.b	\|- B = ( Base ` R )
4		rrhf.k	\|- K = ( TopOpen ` R )
5		rrhf.z	\|- Z = ( ZMod ` R )
6		rrhf.1	\|- ( ph -> R e. DivRing )
7		rrhf.2	\|- ( ph -> R e. NrmRing )
8		rrhf.3	\|- ( ph -> Z e. NrmMod )
9		rrhf.4	\|- ( ph -> ( chr ` R ) = 0 )
10		rrhf.5	\|- ( ph -> R e. CUnifSp )
11		rrhf.6	\|- ( ph -> ( UnifSt ` R ) = ( metUnif ` D ) )
12		nrgngp	\|- ( R e. NrmRing -> R e. NrmGrp )
13		ngpxms	\|- ( R e. NrmGrp -> R e. *MetSp )
14	7 12 13	3syl	\|- ( ph -> R e. *MetSp )
15		xmstps	\|- ( R e. *MetSp -> R e. TopSp )
16	14 15	syl	\|- ( ph -> R e. TopSp )
17	2 4	rrhval	\|- ( R e. TopSp -> ( RRHom ` R ) = ( ( J CnExt K ) ` ( QQHom ` R ) ) )
18	16 17	syl	\|- ( ph -> ( RRHom ` R ) = ( ( J CnExt K ) ` ( QQHom ` R ) ) )
19		rebase	\|- RR = ( Base ` RRfld )
20		retopn	\|- ( topGen ` ran (,) ) = ( TopOpen ` RRfld )
21	2 20	eqtri	\|- J = ( TopOpen ` RRfld )
22		eqid	\|- ( UnifSt ` RRfld ) = ( UnifSt ` RRfld )
23		df-refld	\|- RRfld = ( CCfld \|`s RR )
24	23	oveq1i	\|- ( RRfld \|`s QQ ) = ( ( CCfld \|`s RR ) \|`s QQ )
25		reex	\|- RR e. _V
26		qssre	\|- QQ C_ RR
27		ressabs	\|- ( ( RR e. _V /\ QQ C_ RR ) -> ( ( CCfld \|`s RR ) \|`s QQ ) = ( CCfld \|`s QQ ) )
28	25 26 27	mp2an	\|- ( ( CCfld \|`s RR ) \|`s QQ ) = ( CCfld \|`s QQ )
29	24 28	eqtr2i	\|- ( CCfld \|`s QQ ) = ( RRfld \|`s QQ )
30	29	fveq2i	\|- ( UnifSt ` ( CCfld \|`s QQ ) ) = ( UnifSt ` ( RRfld \|`s QQ ) )
31		eqid	\|- ( UnifSt ` R ) = ( UnifSt ` R )
32		recms	\|- RRfld e. CMetSp
33		cmsms	\|- ( RRfld e. CMetSp -> RRfld e. MetSp )
34		mstps	\|- ( RRfld e. MetSp -> RRfld e. TopSp )
35	32 33 34	mp2b	\|- RRfld e. TopSp
36	35	a1i	\|- ( ph -> RRfld e. TopSp )
37		recusp	\|- RRfld e. CUnifSp
38		cuspusp	\|- ( RRfld e. CUnifSp -> RRfld e. UnifSp )
39	37 38	mp1i	\|- ( ph -> RRfld e. UnifSp )
40	4 3 1	xmstopn	\|- ( R e. *MetSp -> K = ( MetOpen ` D ) )
41	14 40	syl	\|- ( ph -> K = ( MetOpen ` D ) )
42	3 1	xmsxmet	\|- ( R e. MetSp -> D e. ( Met ` B ) )
43		eqid	\|- ( MetOpen ` D ) = ( MetOpen ` D )
44	43	methaus	\|- ( D e. ( *Met ` B ) -> ( MetOpen ` D ) e. Haus )
45	14 42 44	3syl	\|- ( ph -> ( MetOpen ` D ) e. Haus )
46	41 45	eqeltrd	\|- ( ph -> K e. Haus )
47	26	a1i	\|- ( ph -> QQ C_ RR )
48		eqid	\|- ( CCfld \|`s QQ ) = ( CCfld \|`s QQ )
49		eqid	\|- ( UnifSt ` ( CCfld \|`s QQ ) ) = ( UnifSt ` ( CCfld \|`s QQ ) )
50	1	fveq2i	\|- ( metUnif ` D ) = ( metUnif ` ( ( dist ` R ) \|` ( B X. B ) ) )
51	3 48 49 50 5 7 6 8 9	qqhucn	\|- ( ph -> ( QQHom ` R ) e. ( ( UnifSt ` ( CCfld \|`s QQ ) ) uCn ( metUnif ` D ) ) )
52	11	eqcomd	\|- ( ph -> ( metUnif ` D ) = ( UnifSt ` R ) )
53	52	oveq2d	\|- ( ph -> ( ( UnifSt ` ( CCfld \|`s QQ ) ) uCn ( metUnif ` D ) ) = ( ( UnifSt ` ( CCfld \|`s QQ ) ) uCn ( UnifSt ` R ) ) )
54	51 53	eleqtrd	\|- ( ph -> ( QQHom ` R ) e. ( ( UnifSt ` ( CCfld \|`s QQ ) ) uCn ( UnifSt ` R ) ) )
55	2	fveq2i	\|- ( cls ` J ) = ( cls ` ( topGen ` ran (,) ) )
56	55	fveq1i	\|- ( ( cls ` J ) ` QQ ) = ( ( cls ` ( topGen ` ran (,) ) ) ` QQ )
57		qdensere	\|- ( ( cls ` ( topGen ` ran (,) ) ) ` QQ ) = RR
58	56 57	eqtri	\|- ( ( cls ` J ) ` QQ ) = RR
59	58	a1i	\|- ( ph -> ( ( cls ` J ) ` QQ ) = RR )
60	19 3 21 4 22 30 31 36 39 16 10 46 47 54 59	ucnextcn	\|- ( ph -> ( ( J CnExt K ) ` ( QQHom ` R ) ) e. ( J Cn K ) )
61	18 60	eqeltrd	\|- ( ph -> ( RRHom ` R ) e. ( J Cn K ) )

Metamath Proof Explorer

Theorem rrhcn

Proof