![]() |
Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > rrhf | Structured version Visualization version GIF version |
Description: If the topology of 𝑅 is Hausdorff, Cauchy sequences have at most one limit, i.e. the canonical homomorphism of ℝ into 𝑅 is a function. (Contributed by Thierry Arnoux, 2-Nov-2017.) |
Ref | Expression |
---|---|
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‘𝐷)) |
Ref | Expression |
---|---|
rrhf | ⊢ (𝜑 → (ℝHom‘𝑅):ℝ⟶𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rrhf.d | . . . 4 ⊢ 𝐷 = ((dist‘𝑅) ↾ (𝐵 × 𝐵)) | |
2 | eqid 2759 | . . . 4 ⊢ (topGen‘ran (,)) = (topGen‘ran (,)) | |
3 | rrhf.b | . . . 4 ⊢ 𝐵 = (Base‘𝑅) | |
4 | rrhf.k | . . . 4 ⊢ 𝐾 = (TopOpen‘𝑅) | |
5 | rrhf.z | . . . 4 ⊢ 𝑍 = (ℤMod‘𝑅) | |
6 | rrhf.1 | . . . 4 ⊢ (𝜑 → 𝑅 ∈ DivRing) | |
7 | rrhf.2 | . . . 4 ⊢ (𝜑 → 𝑅 ∈ NrmRing) | |
8 | rrhf.3 | . . . 4 ⊢ (𝜑 → 𝑍 ∈ NrmMod) | |
9 | rrhf.4 | . . . 4 ⊢ (𝜑 → (chr‘𝑅) = 0) | |
10 | rrhf.5 | . . . 4 ⊢ (𝜑 → 𝑅 ∈ CUnifSp) | |
11 | rrhf.6 | . . . 4 ⊢ (𝜑 → (UnifSt‘𝑅) = (metUnif‘𝐷)) | |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 | rrhcn 31451 | . . 3 ⊢ (𝜑 → (ℝHom‘𝑅) ∈ ((topGen‘ran (,)) Cn 𝐾)) |
13 | uniretop 23449 | . . . 4 ⊢ ℝ = ∪ (topGen‘ran (,)) | |
14 | eqid 2759 | . . . 4 ⊢ ∪ 𝐾 = ∪ 𝐾 | |
15 | 13, 14 | cnf 21931 | . . 3 ⊢ ((ℝHom‘𝑅) ∈ ((topGen‘ran (,)) Cn 𝐾) → (ℝHom‘𝑅):ℝ⟶∪ 𝐾) |
16 | 12, 15 | syl 17 | . 2 ⊢ (𝜑 → (ℝHom‘𝑅):ℝ⟶∪ 𝐾) |
17 | nrgngp 23349 | . . . . 5 ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp) | |
18 | ngpxms 23288 | . . . . 5 ⊢ (𝑅 ∈ NrmGrp → 𝑅 ∈ ∞MetSp) | |
19 | 7, 17, 18 | 3syl 18 | . . . 4 ⊢ (𝜑 → 𝑅 ∈ ∞MetSp) |
20 | xmstps 23140 | . . . 4 ⊢ (𝑅 ∈ ∞MetSp → 𝑅 ∈ TopSp) | |
21 | 3, 4 | tpsuni 21621 | . . . 4 ⊢ (𝑅 ∈ TopSp → 𝐵 = ∪ 𝐾) |
22 | 19, 20, 21 | 3syl 18 | . . 3 ⊢ (𝜑 → 𝐵 = ∪ 𝐾) |
23 | 22 | feq3d 6478 | . 2 ⊢ (𝜑 → ((ℝHom‘𝑅):ℝ⟶𝐵 ↔ (ℝHom‘𝑅):ℝ⟶∪ 𝐾)) |
24 | 16, 23 | mpbird 260 | 1 ⊢ (𝜑 → (ℝHom‘𝑅):ℝ⟶𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2112 ∪ cuni 4791 × cxp 5515 ran crn 5518 ↾ cres 5519 ⟶wf 6324 ‘cfv 6328 (class class class)co 7143 ℝcr 10559 0cc0 10560 (,)cioo 12764 Basecbs 16526 distcds 16617 TopOpenctopn 16738 topGenctg 16754 DivRingcdr 19555 metUnifcmetu 20142 ℤModczlm 20255 chrcchr 20256 TopSpctps 21617 Cn ccn 21909 UnifStcuss 22939 CUnifSpccusp 22983 ∞MetSpcxms 23004 NrmGrpcngp 23264 NrmRingcnrg 23266 NrmModcnlm 23267 ℝHomcrrh 31447 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-rep 5149 ax-sep 5162 ax-nul 5169 ax-pow 5227 ax-pr 5291 ax-un 7452 ax-cnex 10616 ax-resscn 10617 ax-1cn 10618 ax-icn 10619 ax-addcl 10620 ax-addrcl 10621 ax-mulcl 10622 ax-mulrcl 10623 ax-mulcom 10624 ax-addass 10625 ax-mulass 10626 ax-distr 10627 ax-i2m1 10628 ax-1ne0 10629 ax-1rid 10630 ax-rnegex 10631 ax-rrecex 10632 ax-cnre 10633 ax-pre-lttri 10634 ax-pre-lttrn 10635 ax-pre-ltadd 10636 ax-pre-mulgt0 10637 ax-pre-sup 10638 ax-addf 10639 ax-mulf 10640 |
This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2071 df-mo 2558 df-eu 2589 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2899 df-ne 2950 df-nel 3054 df-ral 3073 df-rex 3074 df-reu 3075 df-rmo 3076 df-rab 3077 df-v 3409 df-sbc 3694 df-csb 3802 df-dif 3857 df-un 3859 df-in 3861 df-ss 3871 df-pss 3873 df-nul 4222 df-if 4414 df-pw 4489 df-sn 4516 df-pr 4518 df-tp 4520 df-op 4522 df-uni 4792 df-int 4832 df-iun 4878 df-iin 4879 df-br 5026 df-opab 5088 df-mpt 5106 df-tr 5132 df-id 5423 df-eprel 5428 df-po 5436 df-so 5437 df-fr 5476 df-se 5477 df-we 5478 df-xp 5523 df-rel 5524 df-cnv 5525 df-co 5526 df-dm 5527 df-rn 5528 df-res 5529 df-ima 5530 df-pred 6119 df-ord 6165 df-on 6166 df-lim 6167 df-suc 6168 df-iota 6287 df-fun 6330 df-fn 6331 df-f 6332 df-f1 6333 df-fo 6334 df-f1o 6335 df-fv 6336 df-isom 6337 df-riota 7101 df-ov 7146 df-oprab 7147 df-mpo 7148 df-of 7398 df-om 7573 df-1st 7686 df-2nd 7687 df-supp 7829 df-tpos 7895 df-wrecs 7950 df-recs 8011 df-rdg 8049 df-1o 8105 df-2o 8106 df-oadd 8109 df-er 8292 df-map 8411 df-pm 8412 df-ixp 8473 df-en 8521 df-dom 8522 df-sdom 8523 df-fin 8524 df-fsupp 8852 df-fi 8893 df-sup 8924 df-inf 8925 df-oi 8992 df-card 9386 df-pnf 10700 df-mnf 10701 df-xr 10702 df-ltxr 10703 df-le 10704 df-sub 10895 df-neg 10896 df-div 11321 df-nn 11660 df-2 11722 df-3 11723 df-4 11724 df-5 11725 df-6 11726 df-7 11727 df-8 11728 df-9 11729 df-n0 11920 df-z 12006 df-dec 12123 df-uz 12268 df-q 12374 df-rp 12416 df-xneg 12533 df-xadd 12534 df-xmul 12535 df-ioo 12768 df-ico 12770 df-icc 12771 df-fz 12925 df-fzo 13068 df-fl 13196 df-mod 13272 df-seq 13404 df-exp 13465 df-hash 13726 df-cj 14491 df-re 14492 df-im 14493 df-sqrt 14627 df-abs 14628 df-dvds 15641 df-gcd 15879 df-numer 16115 df-denom 16116 df-gz 16306 df-struct 16528 df-ndx 16529 df-slot 16530 df-base 16532 df-sets 16533 df-ress 16534 df-plusg 16621 df-mulr 16622 df-starv 16623 df-sca 16624 df-vsca 16625 df-ip 16626 df-tset 16627 df-ple 16628 df-ds 16630 df-unif 16631 df-hom 16632 df-cco 16633 df-rest 16739 df-topn 16740 df-0g 16758 df-gsum 16759 df-topgen 16760 df-pt 16761 df-prds 16764 df-xrs 16818 df-qtop 16823 df-imas 16824 df-xps 16826 df-mre 16900 df-mrc 16901 df-acs 16903 df-mgm 17903 df-sgrp 17952 df-mnd 17963 df-mhm 18007 df-submnd 18008 df-grp 18157 df-minusg 18158 df-sbg 18159 df-mulg 18277 df-subg 18328 df-ghm 18408 df-cntz 18499 df-od 18708 df-cmn 18960 df-abl 18961 df-mgp 19293 df-ur 19305 df-ring 19352 df-cring 19353 df-oppr 19429 df-dvdsr 19447 df-unit 19448 df-invr 19478 df-dvr 19489 df-rnghom 19523 df-drng 19557 df-subrg 19586 df-abv 19641 df-lmod 19689 df-nzr 20084 df-psmet 20143 df-xmet 20144 df-met 20145 df-bl 20146 df-mopn 20147 df-fbas 20148 df-fg 20149 df-metu 20150 df-cnfld 20152 df-zring 20224 df-zrh 20258 df-zlm 20259 df-chr 20260 df-refld 20355 df-top 21579 df-topon 21596 df-topsp 21618 df-bases 21631 df-cld 21704 df-ntr 21705 df-cls 21706 df-nei 21783 df-cn 21912 df-cnp 21913 df-haus 22000 df-reg 22001 df-cmp 22072 df-tx 22247 df-hmeo 22440 df-fil 22531 df-fm 22623 df-flim 22624 df-flf 22625 df-fcls 22626 df-cnext 22745 df-ust 22886 df-utop 22917 df-uss 22942 df-usp 22943 df-ucn 22962 df-cfilu 22973 df-cusp 22984 df-xms 23007 df-ms 23008 df-tms 23009 df-nm 23269 df-ngp 23270 df-nrg 23272 df-nlm 23273 df-cncf 23564 df-cfil 23940 df-cmet 23942 df-cms 24020 df-qqh 31427 df-rrh 31449 |
This theorem is referenced by: rrhfe 31466 sitgclg 31813 |
Copyright terms: Public domain | W3C validator |