Metamath Proof Explorer

Theorem cmetcusp

Description: The uniform space generated by a complete metric is a complete uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017)

Ref Expression
Assertion cmetcusp ⊢X≠∅∧D∈CMet⁡X→toUnifSp⁡metUnif⁡D∈CUnifSp

Proof

Step Hyp Ref Expression
1 cmetmet ⊢D∈CMet⁡X→D∈Met⁡X
2 metxmet ⊢D∈Met⁡X→D∈∞Met⁡X
3 xmetpsmet ⊢D∈∞Met⁡X→D∈PsMet⁡X
4 1 2 3 3syl ⊢D∈CMet⁡X→D∈PsMet⁡X
5 4 anim2i ⊢X≠∅∧D∈CMet⁡X→X≠∅∧D∈PsMet⁡X
6 metuust ⊢X≠∅∧D∈PsMet⁡X→metUnif⁡D∈UnifOn⁡X
7 eqid ⊢toUnifSp⁡metUnif⁡D=toUnifSp⁡metUnif⁡D
8 7 tususp ⊢metUnif⁡D∈UnifOn⁡X→toUnifSp⁡metUnif⁡D∈UnifSp
9 5 6 8 3syl ⊢X≠∅∧D∈CMet⁡X→toUnifSp⁡metUnif⁡D∈UnifSp
10 simpll ⊢X≠∅∧D∈CMet⁡X∧c∈Fil⁡BasetoUnifSp⁡metUnif⁡D∧c∈CauFilU⁡UnifSt⁡toUnifSp⁡metUnif⁡D→X≠∅∧D∈CMet⁡X
11 10 simprd ⊢X≠∅∧D∈CMet⁡X∧c∈Fil⁡BasetoUnifSp⁡metUnif⁡D∧c∈CauFilU⁡UnifSt⁡toUnifSp⁡metUnif⁡D→D∈CMet⁡X
12 1 2 syl ⊢D∈CMet⁡X→D∈∞Met⁡X
13 12 ad3antlr ⊢X≠∅∧D∈CMet⁡X∧c∈Fil⁡BasetoUnifSp⁡metUnif⁡D∧c∈CauFilU⁡UnifSt⁡toUnifSp⁡metUnif⁡D→D∈∞Met⁡X
14 7 tusbas ⊢metUnif⁡D∈UnifOn⁡X→X=BasetoUnifSp⁡metUnif⁡D
15 14 fveq2d ⊢metUnif⁡D∈UnifOn⁡X→Fil⁡X=Fil⁡BasetoUnifSp⁡metUnif⁡D
16 15 eleq2d ⊢metUnif⁡D∈UnifOn⁡X→c∈Fil⁡X↔c∈Fil⁡BasetoUnifSp⁡metUnif⁡D
17 5 6 16 3syl ⊢X≠∅∧D∈CMet⁡X→c∈Fil⁡X↔c∈Fil⁡BasetoUnifSp⁡metUnif⁡D
18 17 biimpar ⊢X≠∅∧D∈CMet⁡X∧c∈Fil⁡BasetoUnifSp⁡metUnif⁡D→c∈Fil⁡X
19 18 adantr ⊢X≠∅∧D∈CMet⁡X∧c∈Fil⁡BasetoUnifSp⁡metUnif⁡D∧c∈CauFilU⁡UnifSt⁡toUnifSp⁡metUnif⁡D→c∈Fil⁡X
20 7 tususs ⊢metUnif⁡D∈UnifOn⁡X→metUnif⁡D=UnifSt⁡toUnifSp⁡metUnif⁡D
21 20 fveq2d ⊢metUnif⁡D∈UnifOn⁡X→CauFilU⁡metUnif⁡D=CauFilU⁡UnifSt⁡toUnifSp⁡metUnif⁡D
22 5 6 21 3syl ⊢X≠∅∧D∈CMet⁡X→CauFilU⁡metUnif⁡D=CauFilU⁡UnifSt⁡toUnifSp⁡metUnif⁡D
23 22 eleq2d ⊢X≠∅∧D∈CMet⁡X→c∈CauFilU⁡metUnif⁡D↔c∈CauFilU⁡UnifSt⁡toUnifSp⁡metUnif⁡D
24 23 biimpar ⊢X≠∅∧D∈CMet⁡X∧c∈CauFilU⁡UnifSt⁡toUnifSp⁡metUnif⁡D→c∈CauFilU⁡metUnif⁡D
25 24 adantlr ⊢X≠∅∧D∈CMet⁡X∧c∈Fil⁡BasetoUnifSp⁡metUnif⁡D∧c∈CauFilU⁡UnifSt⁡toUnifSp⁡metUnif⁡D→c∈CauFilU⁡metUnif⁡D
26 cfilucfil2 ⊢X≠∅∧D∈PsMet⁡X→c∈CauFilU⁡metUnif⁡D↔c∈fBas⁡X∧∀x∈ℝ+∃y∈cDy×y⊆0x
27 5 26 syl ⊢X≠∅∧D∈CMet⁡X→c∈CauFilU⁡metUnif⁡D↔c∈fBas⁡X∧∀x∈ℝ+∃y∈cDy×y⊆0x
28 27 simplbda ⊢X≠∅∧D∈CMet⁡X∧c∈CauFilU⁡metUnif⁡D→∀x∈ℝ+∃y∈cDy×y⊆0x
29 10 25 28 syl2anc ⊢X≠∅∧D∈CMet⁡X∧c∈Fil⁡BasetoUnifSp⁡metUnif⁡D∧c∈CauFilU⁡UnifSt⁡toUnifSp⁡metUnif⁡D→∀x∈ℝ+∃y∈cDy×y⊆0x
30 iscfil ⊢D∈∞Met⁡X→c∈CauFil⁡D↔c∈Fil⁡X∧∀x∈ℝ+∃y∈cDy×y⊆0x
31 30 biimpar ⊢D∈∞Met⁡X∧c∈Fil⁡X∧∀x∈ℝ+∃y∈cDy×y⊆0x→c∈CauFil⁡D
32 13 19 29 31 syl12anc ⊢X≠∅∧D∈CMet⁡X∧c∈Fil⁡BasetoUnifSp⁡metUnif⁡D∧c∈CauFilU⁡UnifSt⁡toUnifSp⁡metUnif⁡D→c∈CauFil⁡D
33 eqid ⊢MetOpen⁡D=MetOpen⁡D
34 33 cmetcvg ⊢D∈CMet⁡X∧c∈CauFil⁡D→MetOpen⁡DfLimc≠∅
35 11 32 34 syl2anc ⊢X≠∅∧D∈CMet⁡X∧c∈Fil⁡BasetoUnifSp⁡metUnif⁡D∧c∈CauFilU⁡UnifSt⁡toUnifSp⁡metUnif⁡D→MetOpen⁡DfLimc≠∅
36 eqid ⊢unifTop⁡metUnif⁡D=unifTop⁡metUnif⁡D
37 7 36 tustopn ⊢metUnif⁡D∈UnifOn⁡X→unifTop⁡metUnif⁡D=TopOpen⁡toUnifSp⁡metUnif⁡D
38 5 6 37 3syl ⊢X≠∅∧D∈CMet⁡X→unifTop⁡metUnif⁡D=TopOpen⁡toUnifSp⁡metUnif⁡D
39 12 anim2i ⊢X≠∅∧D∈CMet⁡X→X≠∅∧D∈∞Met⁡X
40 xmetutop ⊢X≠∅∧D∈∞Met⁡X→unifTop⁡metUnif⁡D=MetOpen⁡D
41 39 40 syl ⊢X≠∅∧D∈CMet⁡X→unifTop⁡metUnif⁡D=MetOpen⁡D
42 38 41 eqtr3d ⊢X≠∅∧D∈CMet⁡X→TopOpen⁡toUnifSp⁡metUnif⁡D=MetOpen⁡D
43 42 oveq1d ⊢X≠∅∧D∈CMet⁡X→TopOpen⁡toUnifSp⁡metUnif⁡DfLimc=MetOpen⁡DfLimc
44 43 neeq1d ⊢X≠∅∧D∈CMet⁡X→TopOpen⁡toUnifSp⁡metUnif⁡DfLimc≠∅↔MetOpen⁡DfLimc≠∅
45 44 biimpar ⊢X≠∅∧D∈CMet⁡X∧MetOpen⁡DfLimc≠∅→TopOpen⁡toUnifSp⁡metUnif⁡DfLimc≠∅
46 10 35 45 syl2anc ⊢X≠∅∧D∈CMet⁡X∧c∈Fil⁡BasetoUnifSp⁡metUnif⁡D∧c∈CauFilU⁡UnifSt⁡toUnifSp⁡metUnif⁡D→TopOpen⁡toUnifSp⁡metUnif⁡DfLimc≠∅
47 46 ex ⊢X≠∅∧D∈CMet⁡X∧c∈Fil⁡BasetoUnifSp⁡metUnif⁡D→c∈CauFilU⁡UnifSt⁡toUnifSp⁡metUnif⁡D→TopOpen⁡toUnifSp⁡metUnif⁡DfLimc≠∅
48 47 ralrimiva ⊢X≠∅∧D∈CMet⁡X→∀c∈Fil⁡BasetoUnifSp⁡metUnif⁡Dc∈CauFilU⁡UnifSt⁡toUnifSp⁡metUnif⁡D→TopOpen⁡toUnifSp⁡metUnif⁡DfLimc≠∅
49 iscusp ⊢toUnifSp⁡metUnif⁡D∈CUnifSp↔toUnifSp⁡metUnif⁡D∈UnifSp∧∀c∈Fil⁡BasetoUnifSp⁡metUnif⁡Dc∈CauFilU⁡UnifSt⁡toUnifSp⁡metUnif⁡D→TopOpen⁡toUnifSp⁡metUnif⁡DfLimc≠∅
50 9 48 49 sylanbrc ⊢X≠∅∧D∈CMet⁡X→toUnifSp⁡metUnif⁡D∈CUnifSp