Metamath Proof Explorer


Theorem psmetutop

Description: The topology induced by a uniform structure generated by a metric D is generated by that metric's open balls. (Contributed by Thierry Arnoux, 6-Dec-2017) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion psmetutop X D PsMet X unifTop metUnif D = topGen ran ball D

Proof

Step Hyp Ref Expression
1 metuust X D PsMet X metUnif D UnifOn X
2 utopval metUnif D UnifOn X unifTop metUnif D = a 𝒫 X | x a v metUnif D v x a
3 1 2 syl X D PsMet X unifTop metUnif D = a 𝒫 X | x a v metUnif D v x a
4 3 eleq2d X D PsMet X a unifTop metUnif D a a 𝒫 X | x a v metUnif D v x a
5 rabid a a 𝒫 X | x a v metUnif D v x a a 𝒫 X x a v metUnif D v x a
6 4 5 bitrdi X D PsMet X a unifTop metUnif D a 𝒫 X x a v metUnif D v x a
7 6 biimpa X D PsMet X a unifTop metUnif D a 𝒫 X x a v metUnif D v x a
8 7 simpld X D PsMet X a unifTop metUnif D a 𝒫 X
9 8 elpwid X D PsMet X a unifTop metUnif D a X
10 unirnblps D PsMet X ran ball D = X
11 10 ad2antlr X D PsMet X a unifTop metUnif D ran ball D = X
12 9 11 sseqtrrd X D PsMet X a unifTop metUnif D a ran ball D
13 simpr X D PsMet X a unifTop metUnif D x a v metUnif D v x a v x a
14 simp-5r X D PsMet X a unifTop metUnif D x a v metUnif D v x a D PsMet X
15 simplr X D PsMet X a unifTop metUnif D x a v metUnif D v x a v metUnif D
16 9 ad3antrrr X D PsMet X a unifTop metUnif D x a v metUnif D v x a a X
17 simpllr X D PsMet X a unifTop metUnif D x a v metUnif D v x a x a
18 16 17 sseldd X D PsMet X a unifTop metUnif D x a v metUnif D v x a x X
19 metustbl D PsMet X v metUnif D x X b ran ball D x b b v x
20 14 15 18 19 syl3anc X D PsMet X a unifTop metUnif D x a v metUnif D v x a b ran ball D x b b v x
21 sstr b v x v x a b a
22 21 expcom v x a b v x b a
23 22 anim2d v x a x b b v x x b b a
24 23 reximdv v x a b ran ball D x b b v x b ran ball D x b b a
25 13 20 24 sylc X D PsMet X a unifTop metUnif D x a v metUnif D v x a b ran ball D x b b a
26 7 simprd X D PsMet X a unifTop metUnif D x a v metUnif D v x a
27 26 r19.21bi X D PsMet X a unifTop metUnif D x a v metUnif D v x a
28 25 27 r19.29a X D PsMet X a unifTop metUnif D x a b ran ball D x b b a
29 28 ralrimiva X D PsMet X a unifTop metUnif D x a b ran ball D x b b a
30 12 29 jca X D PsMet X a unifTop metUnif D a ran ball D x a b ran ball D x b b a
31 fvex ball D V
32 31 rnex ran ball D V
33 eltg2 ran ball D V a topGen ran ball D a ran ball D x a b ran ball D x b b a
34 32 33 mp1i X D PsMet X a unifTop metUnif D a topGen ran ball D a ran ball D x a b ran ball D x b b a
35 30 34 mpbird X D PsMet X a unifTop metUnif D a topGen ran ball D
36 32 33 mp1i X D PsMet X a topGen ran ball D a ran ball D x a b ran ball D x b b a
37 36 biimpa X D PsMet X a topGen ran ball D a ran ball D x a b ran ball D x b b a
38 37 simpld X D PsMet X a topGen ran ball D a ran ball D
39 10 ad2antlr X D PsMet X a topGen ran ball D ran ball D = X
40 38 39 sseqtrd X D PsMet X a topGen ran ball D a X
41 elpwg a topGen ran ball D a 𝒫 X a X
42 41 adantl X D PsMet X a topGen ran ball D a 𝒫 X a X
43 40 42 mpbird X D PsMet X a topGen ran ball D a 𝒫 X
44 simpllr X D PsMet X a topGen ran ball D x a D PsMet X
45 40 sselda X D PsMet X a topGen ran ball D x a x X
46 37 simprd X D PsMet X a topGen ran ball D x a b ran ball D x b b a
47 46 r19.21bi X D PsMet X a topGen ran ball D x a b ran ball D x b b a
48 blssexps D PsMet X x X b ran ball D x b b a d + x ball D d a
49 44 45 48 syl2anc X D PsMet X a topGen ran ball D x a b ran ball D x b b a d + x ball D d a
50 47 49 mpbid X D PsMet X a topGen ran ball D x a d + x ball D d a
51 blval2 D PsMet X x X d + x ball D d = D -1 0 d x
52 51 3expa D PsMet X x X d + x ball D d = D -1 0 d x
53 52 sseq1d D PsMet X x X d + x ball D d a D -1 0 d x a
54 53 rexbidva D PsMet X x X d + x ball D d a d + D -1 0 d x a
55 54 biimpa D PsMet X x X d + x ball D d a d + D -1 0 d x a
56 44 45 50 55 syl21anc X D PsMet X a topGen ran ball D x a d + D -1 0 d x a
57 cnvexg D PsMet X D -1 V
58 imaexg D -1 V D -1 0 d V
59 57 58 syl D PsMet X D -1 0 d V
60 59 ralrimivw D PsMet X d + D -1 0 d V
61 eqid d + D -1 0 d = d + D -1 0 d
62 imaeq1 v = D -1 0 d v x = D -1 0 d x
63 62 sseq1d v = D -1 0 d v x a D -1 0 d x a
64 61 63 rexrnmptw d + D -1 0 d V v ran d + D -1 0 d v x a d + D -1 0 d x a
65 44 60 64 3syl X D PsMet X a topGen ran ball D x a v ran d + D -1 0 d v x a d + D -1 0 d x a
66 56 65 mpbird X D PsMet X a topGen ran ball D x a v ran d + D -1 0 d v x a
67 oveq2 d = e 0 d = 0 e
68 67 imaeq2d d = e D -1 0 d = D -1 0 e
69 68 cbvmptv d + D -1 0 d = e + D -1 0 e
70 69 rneqi ran d + D -1 0 d = ran e + D -1 0 e
71 70 metustfbas X D PsMet X ran d + D -1 0 d fBas X × X
72 ssfg ran d + D -1 0 d fBas X × X ran d + D -1 0 d X × X filGen ran d + D -1 0 d
73 71 72 syl X D PsMet X ran d + D -1 0 d X × X filGen ran d + D -1 0 d
74 metuval D PsMet X metUnif D = X × X filGen ran d + D -1 0 d
75 74 adantl X D PsMet X metUnif D = X × X filGen ran d + D -1 0 d
76 73 75 sseqtrrd X D PsMet X ran d + D -1 0 d metUnif D
77 ssrexv ran d + D -1 0 d metUnif D v ran d + D -1 0 d v x a v metUnif D v x a
78 76 77 syl X D PsMet X v ran d + D -1 0 d v x a v metUnif D v x a
79 78 ad2antrr X D PsMet X a topGen ran ball D x a v ran d + D -1 0 d v x a v metUnif D v x a
80 66 79 mpd X D PsMet X a topGen ran ball D x a v metUnif D v x a
81 80 ralrimiva X D PsMet X a topGen ran ball D x a v metUnif D v x a
82 43 81 jca X D PsMet X a topGen ran ball D a 𝒫 X x a v metUnif D v x a
83 6 biimpar X D PsMet X a 𝒫 X x a v metUnif D v x a a unifTop metUnif D
84 82 83 syldan X D PsMet X a topGen ran ball D a unifTop metUnif D
85 35 84 impbida X D PsMet X a unifTop metUnif D a topGen ran ball D
86 85 eqrdv X D PsMet X unifTop metUnif D = topGen ran ball D