Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rrhcn Structured version   Unicode version

Theorem rrhcn 26557
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.)
Hypotheses
Ref Expression
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
Ref Expression
rrhcn  |-  ( ph  ->  (RRHom `  R )  e.  ( J  Cn  K
) )

Proof of Theorem rrhcn
StepHypRef Expression
1 rrhf.2 . . . . 5  |-  ( ph  ->  R  e. NrmRing )
2 nrgngp 20356 . . . . 5  |-  ( R  e. NrmRing  ->  R  e. NrmGrp )
3 ngpxms 20306 . . . . 5  |-  ( R  e. NrmGrp  ->  R  e.  *MetSp )
41, 2, 33syl 20 . . . 4  |-  ( ph  ->  R  e.  *MetSp )
5 xmstps 20141 . . . 4  |-  ( R  e.  *MetSp  ->  R  e.  TopSp )
64, 5syl 16 . . 3  |-  ( ph  ->  R  e.  TopSp )
7 rrhf.j . . . 4  |-  J  =  ( topGen `  ran  (,) )
8 rrhf.k . . . 4  |-  K  =  ( TopOpen `  R )
97, 8rrhval 26556 . . 3  |-  ( R  e.  TopSp  ->  (RRHom `  R
)  =  ( ( JCnExt K ) `  (QQHom `  R ) ) )
106, 9syl 16 . 2  |-  ( ph  ->  (RRHom `  R )  =  ( ( JCnExt
K ) `  (QQHom `  R ) ) )
11 rebase 18142 . . 3  |-  RR  =  ( Base ` RRfld )
12 rrhf.b . . 3  |-  B  =  ( Base `  R
)
13 retopn 20996 . . . 4  |-  ( topGen ` 
ran  (,) )  =  (
TopOpen ` RRfld )
14 eqid 2451 . . . 4  |-  ( TopOpen ` RRfld )  =  ( TopOpen ` RRfld )
157, 13, 143eqtri 2483 . . 3  |-  J  =  ( TopOpen ` RRfld )
16 eqid 2451 . . 3  |-  (UnifSt ` RRfld )  =  (UnifSt ` RRfld )
17 df-refld 18141 . . . . . 6  |- RRfld  =  (flds  RR )
1817oveq1i 6197 . . . . 5  |-  (RRfld ↾s  QQ )  =  ( (flds  RR )s  QQ )
19 reex 9471 . . . . . 6  |-  RR  e.  _V
20 qssre 11061 . . . . . 6  |-  QQ  C_  RR
21 ressabs 14335 . . . . . 6  |-  ( ( RR  e.  _V  /\  QQ  C_  RR )  -> 
( (flds  RR )s  QQ )  =  (flds  QQ ) )
2219, 20, 21mp2an 672 . . . . 5  |-  ( (flds  RR )s  QQ )  =  (flds  QQ )
2318, 22eqtr2i 2480 . . . 4  |-  (flds  QQ )  =  (RRfld ↾s  QQ )
2423fveq2i 5789 . . 3  |-  (UnifSt `  (flds  QQ ) )  =  (UnifSt `  (RRfld ↾s 
QQ ) )
25 eqid 2451 . . 3  |-  (UnifSt `  R )  =  (UnifSt `  R )
26 recms 20997 . . . . 5  |- RRfld  e. CMetSp
27 cmsms 20972 . . . . 5  |-  (RRfld  e. CMetSp  -> RRfld  e. 
MetSp )
28 mstps 20143 . . . . 5  |-  (RRfld  e.  MetSp  -> RRfld 
e.  TopSp )
2926, 27, 28mp2b 10 . . . 4  |- RRfld  e.  TopSp
3029a1i 11 . . 3  |-  ( ph  -> RRfld 
e.  TopSp )
31 recusp 20999 . . . . 5  |- RRfld  e. CUnifSp
32 cuspusp 19988 . . . . 5  |-  (RRfld  e. CUnifSp  -> RRfld  e. UnifSp
)
3331, 32ax-mp 5 . . . 4  |- RRfld  e. UnifSp
3433a1i 11 . . 3  |-  ( ph  -> RRfld 
e. UnifSp )
35 rrhf.5 . . 3  |-  ( ph  ->  R  e. CUnifSp )
36 rrhf.d . . . . . 6  |-  D  =  ( ( dist `  R
)  |`  ( B  X.  B ) )
378, 12, 36xmstopn 20139 . . . . 5  |-  ( R  e.  *MetSp  ->  K  =  ( MetOpen `  D
) )
384, 37syl 16 . . . 4  |-  ( ph  ->  K  =  ( MetOpen `  D ) )
3912, 36xmsxmet 20144 . . . . 5  |-  ( R  e.  *MetSp  ->  D  e.  ( *Met `  B ) )
40 eqid 2451 . . . . . 6  |-  ( MetOpen `  D )  =  (
MetOpen `  D )
4140methaus 20208 . . . . 5  |-  ( D  e.  ( *Met `  B )  ->  ( MetOpen
`  D )  e. 
Haus )
424, 39, 413syl 20 . . . 4  |-  ( ph  ->  ( MetOpen `  D )  e.  Haus )
4338, 42eqeltrd 2537 . . 3  |-  ( ph  ->  K  e.  Haus )
4420a1i 11 . . 3  |-  ( ph  ->  QQ  C_  RR )
45 eqid 2451 . . . . 5  |-  (flds  QQ )  =  (flds  QQ )
46 eqid 2451 . . . . 5  |-  (UnifSt `  (flds  QQ ) )  =  (UnifSt `  (flds  QQ ) )
4736fveq2i 5789 . . . . 5  |-  (metUnif `  D
)  =  (metUnif `  (
( dist `  R )  |`  ( B  X.  B
) ) )
48 eqid 2451 . . . . 5  |-  ( ZMod
`  R )  =  ( ZMod `  R
)
49 rrhf.1 . . . . 5  |-  ( ph  ->  R  e.  DivRing )
50 rrhf.z . . . . . 6  |-  Z  =  ( ZMod `  R
)
51 rrhf.3 . . . . . 6  |-  ( ph  ->  Z  e. NrmMod )
5250, 51syl5eqelr 2542 . . . . 5  |-  ( ph  ->  ( ZMod `  R
)  e. NrmMod )
53 rrhf.4 . . . . 5  |-  ( ph  ->  (chr `  R )  =  0 )
5412, 45, 46, 47, 48, 1, 49, 52, 53qqhucn 26552 . . . 4  |-  ( ph  ->  (QQHom `  R )  e.  ( (UnifSt `  (flds  QQ )
) Cnu (metUnif `  D )
) )
55 rrhf.6 . . . . . 6  |-  ( ph  ->  (UnifSt `  R )  =  (metUnif `  D )
)
5655eqcomd 2458 . . . . 5  |-  ( ph  ->  (metUnif `  D )  =  (UnifSt `  R )
)
5756oveq2d 6203 . . . 4  |-  ( ph  ->  ( (UnifSt `  (flds  QQ )
) Cnu (metUnif `  D )
)  =  ( (UnifSt `  (flds  QQ ) ) Cnu (UnifSt `  R
) ) )
5854, 57eleqtrd 2539 . . 3  |-  ( ph  ->  (QQHom `  R )  e.  ( (UnifSt `  (flds  QQ )
) Cnu (UnifSt `  R )
) )
597fveq2i 5789 . . . . . 6  |-  ( cls `  J )  =  ( cls `  ( topGen ` 
ran  (,) ) )
6059fveq1i 5787 . . . . 5  |-  ( ( cls `  J ) `
 QQ )  =  ( ( cls `  ( topGen `
 ran  (,) )
) `  QQ )
61 qdensere 20462 . . . . 5  |-  ( ( cls `  ( topGen ` 
ran  (,) ) ) `  QQ )  =  RR
6260, 61eqtri 2479 . . . 4  |-  ( ( cls `  J ) `
 QQ )  =  RR
6362a1i 11 . . 3  |-  ( ph  ->  ( ( cls `  J
) `  QQ )  =  RR )
6411, 12, 15, 8, 16, 24, 25, 30, 34, 6, 35, 43, 44, 58, 63ucnextcn 19992 . 2  |-  ( ph  ->  ( ( JCnExt K
) `  (QQHom `  R
) )  e.  ( J  Cn  K ) )
6510, 64eqeltrd 2537 1  |-  ( ph  ->  (RRHom `  R )  e.  ( J  Cn  K
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    e. wcel 1758   _Vcvv 3065    C_ wss 3423    X. cxp 4933   ran crn 4936    |` cres 4937   ` cfv 5513  (class class class)co 6187   RRcr 9379   0cc0 9380   QQcq 11051   (,)cioo 11398   Basecbs 14273   ↾s cress 14274   distcds 14346   TopOpenctopn 14459   topGenctg 14475   DivRingcdr 16935   *Metcxmt 17907   MetOpencmopn 17912  metUnifcmetu 17914  ℂfldccnfld 17924   ZModczlm 18038  chrcchr 18039  RRfldcrefld 18140   TopSpctps 18614   clsccl 18735    Cn ccn 18941   Hauscha 19025  CnExtccnext 19744  UnifStcuss 19941  UnifSpcusp 19942   Cnucucn 19963  CUnifSpccusp 19985   *MetSpcxme 20005   MetSpcmt 20006  NrmGrpcngp 20283  NrmRingcnrg 20285  NrmModcnlm 20286  CMetSpccms 20956  QQHomcqqh 26532  RRHomcrrh 26553
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-rep 4498  ax-sep 4508  ax-nul 4516  ax-pow 4565  ax-pr 4626  ax-un 6469  ax-inf2 7945  ax-cnex 9436  ax-resscn 9437  ax-1cn 9438  ax-icn 9439  ax-addcl 9440  ax-addrcl 9441  ax-mulcl 9442  ax-mulrcl 9443  ax-mulcom 9444  ax-addass 9445  ax-mulass 9446  ax-distr 9447  ax-i2m1 9448  ax-1ne0 9449  ax-1rid 9450  ax-rnegex 9451  ax-rrecex 9452  ax-cnre 9453  ax-pre-lttri 9454  ax-pre-lttrn 9455  ax-pre-ltadd 9456  ax-pre-mulgt0 9457  ax-pre-sup 9458  ax-addf 9459  ax-mulf 9460
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2599  df-ne 2644  df-nel 2645  df-ral 2798  df-rex 2799  df-reu 2800  df-rmo 2801  df-rab 2802  df-v 3067  df-sbc 3282  df-csb 3384  df-dif 3426  df-un 3428  df-in 3430  df-ss 3437  df-pss 3439  df-nul 3733  df-if 3887  df-pw 3957  df-sn 3973  df-pr 3975  df-tp 3977  df-op 3979  df-uni 4187  df-int 4224  df-iun 4268  df-iin 4269  df-br 4388  df-opab 4446  df-mpt 4447  df-tr 4481  df-eprel 4727  df-id 4731  df-po 4736  df-so 4737  df-fr 4774  df-se 4775  df-we 4776  df-ord 4817  df-on 4818  df-lim 4819  df-suc 4820  df-xp 4941  df-rel 4942  df-cnv 4943  df-co 4944  df-dm 4945  df-rn 4946  df-res 4947  df-ima 4948  df-iota 5476  df-fun 5515  df-fn 5516  df-f 5517  df-f1 5518  df-fo 5519  df-f1o 5520  df-fv 5521  df-isom 5522  df-riota 6148  df-ov 6190  df-oprab 6191  df-mpt2 6192  df-of 6417  df-om 6574  df-1st 6674  df-2nd 6675  df-supp 6788  df-tpos 6842  df-recs 6929  df-rdg 6963  df-1o 7017  df-2o 7018  df-oadd 7021  df-er 7198  df-map 7313  df-pm 7314  df-ixp 7361  df-en 7408  df-dom 7409  df-sdom 7410  df-fin 7411  df-fsupp 7719  df-fi 7759  df-sup 7789  df-oi 7822  df-card 8207  df-cda 8435  df-pnf 9518  df-mnf 9519  df-xr 9520  df-ltxr 9521  df-le 9522  df-sub 9695  df-neg 9696  df-div 10092  df-nn 10421  df-2 10478  df-3 10479  df-4 10480  df-5 10481  df-6 10482  df-7 10483  df-8 10484  df-9 10485  df-10 10486  df-n0 10678  df-z 10745  df-dec 10854  df-uz 10960  df-q 11052  df-rp 11090  df-xneg 11187  df-xadd 11188  df-xmul 11189  df-ioo 11402  df-ico 11404  df-icc 11405  df-fz 11536  df-fzo 11647  df-fl 11740  df-mod 11807  df-seq 11905  df-exp 11964  df-hash 12202  df-cj 12687  df-re 12688  df-im 12689  df-sqr 12823  df-abs 12824  df-dvds 13635  df-gcd 13790  df-numer 13912  df-denom 13913  df-gz 14090  df-struct 14275  df-ndx 14276  df-slot 14277  df-base 14278  df-sets 14279  df-ress 14280  df-plusg 14350  df-mulr 14351  df-starv 14352  df-sca 14353  df-vsca 14354  df-ip 14355  df-tset 14356  df-ple 14357  df-ds 14359  df-unif 14360  df-hom 14361  df-cco 14362  df-rest 14460  df-topn 14461  df-0g 14479  df-gsum 14480  df-topgen 14481  df-pt 14482  df-prds 14485  df-xrs 14539  df-qtop 14544  df-imas 14545  df-xps 14547  df-mre 14623  df-mrc 14624  df-acs 14626  df-mnd 15514  df-mhm 15563  df-submnd 15564  df-grp 15644  df-minusg 15645  df-sbg 15646  df-mulg 15647  df-subg 15777  df-ghm 15844  df-cntz 15934  df-od 16133  df-cmn 16380  df-abl 16381  df-mgp 16694  df-ur 16706  df-rng 16750  df-cring 16751  df-oppr 16818  df-dvdsr 16836  df-unit 16837  df-invr 16867  df-dvr 16878  df-rnghom 16909  df-drng 16937  df-subrg 16966  df-abv 17005  df-lmod 17053  df-nzr 17443  df-psmet 17915  df-xmet 17916  df-met 17917  df-bl 17918  df-mopn 17919  df-fbas 17920  df-fg 17921  df-metu 17923  df-cnfld 17925  df-zring 17990  df-zrh 18041  df-zlm 18042  df-chr 18043  df-refld 18141  df-top 18616  df-bases 18618  df-topon 18619  df-topsp 18620  df-cld 18736  df-ntr 18737  df-cls 18738  df-nei 18815  df-cn 18944  df-cnp 18945  df-haus 19032  df-reg 19033  df-cmp 19103  df-tx 19248  df-hmeo 19441  df-fil 19532  df-fm 19624  df-flim 19625  df-flf 19626  df-fcls 19627  df-cnext 19745  df-ust 19888  df-utop 19919  df-uss 19944  df-usp 19945  df-ucn 19964  df-cfilu 19975  df-cusp 19986  df-xms 20008  df-ms 20009  df-tms 20010  df-nm 20288  df-ngp 20289  df-nrg 20291  df-nlm 20292  df-cncf 20567  df-cfil 20879  df-cmet 20881  df-cms 20959  df-qqh 26533  df-rrh 26555
This theorem is referenced by:  rrhf  26558  rrhcne  26572
  Copyright terms: Public domain W3C validator