Metamath Proof Explorer


Theorem restmetu

Description: The uniform structure generated by the restriction of a metric is its trace. (Contributed by Thierry Arnoux, 18-Dec-2017)

Ref Expression
Assertion restmetu A D PsMet X A X metUnif D 𝑡 A × A = metUnif D A × A

Proof

Step Hyp Ref Expression
1 simp1 A D PsMet X A X A
2 psmetres2 D PsMet X A X D A × A PsMet A
3 2 3adant1 A D PsMet X A X D A × A PsMet A
4 oveq2 a = b 0 a = 0 b
5 4 imaeq2d a = b D A × A -1 0 a = D A × A -1 0 b
6 5 cbvmptv a + D A × A -1 0 a = b + D A × A -1 0 b
7 6 rneqi ran a + D A × A -1 0 a = ran b + D A × A -1 0 b
8 7 metustfbas A D A × A PsMet A ran a + D A × A -1 0 a fBas A × A
9 1 3 8 syl2anc A D PsMet X A X ran a + D A × A -1 0 a fBas A × A
10 fgval ran a + D A × A -1 0 a fBas A × A A × A filGen ran a + D A × A -1 0 a = v 𝒫 A × A | ran a + D A × A -1 0 a 𝒫 v
11 9 10 syl A D PsMet X A X A × A filGen ran a + D A × A -1 0 a = v 𝒫 A × A | ran a + D A × A -1 0 a 𝒫 v
12 metuval D A × A PsMet A metUnif D A × A = A × A filGen ran a + D A × A -1 0 a
13 3 12 syl A D PsMet X A X metUnif D A × A = A × A filGen ran a + D A × A -1 0 a
14 fvex metUnif D V
15 3 elfvexd A D PsMet X A X A V
16 15 15 xpexd A D PsMet X A X A × A V
17 restval metUnif D V A × A V metUnif D 𝑡 A × A = ran v metUnif D v A × A
18 14 16 17 sylancr A D PsMet X A X metUnif D 𝑡 A × A = ran v metUnif D v A × A
19 inss2 v A × A A × A
20 sseq1 u = v A × A u A × A v A × A A × A
21 19 20 mpbiri u = v A × A u A × A
22 vex u V
23 22 elpw u 𝒫 A × A u A × A
24 21 23 sylibr u = v A × A u 𝒫 A × A
25 24 rexlimivw v metUnif D u = v A × A u 𝒫 A × A
26 25 adantl A D PsMet X A X v metUnif D u = v A × A u 𝒫 A × A
27 nfv a A D PsMet X A X v metUnif D u = v A × A
28 nfmpt1 _ a a + D -1 0 a
29 28 nfrn _ a ran a + D -1 0 a
30 29 nfcri a w ran a + D -1 0 a
31 27 30 nfan a A D PsMet X A X v metUnif D u = v A × A w ran a + D -1 0 a
32 nfv a w v
33 31 32 nfan a A D PsMet X A X v metUnif D u = v A × A w ran a + D -1 0 a w v
34 nfmpt1 _ a a + D A × A -1 0 a
35 34 nfrn _ a ran a + D A × A -1 0 a
36 nfcv _ a 𝒫 u
37 35 36 nfin _ a ran a + D A × A -1 0 a 𝒫 u
38 nfcv _ a
39 37 38 nfne a ran a + D A × A -1 0 a 𝒫 u
40 simplr A D PsMet X A X v metUnif D u = v A × A w ran a + D -1 0 a w v a + w = D -1 0 a a +
41 ineq1 w = D -1 0 a w A × A = D -1 0 a A × A
42 41 adantl A D PsMet X A X v metUnif D u = v A × A w ran a + D -1 0 a w v a + w = D -1 0 a w A × A = D -1 0 a A × A
43 simp2 A D PsMet X A X D PsMet X
44 psmetf D PsMet X D : X × X *
45 ffun D : X × X * Fun D
46 respreima Fun D D A × A -1 0 a = D -1 0 a A × A
47 43 44 45 46 4syl A D PsMet X A X D A × A -1 0 a = D -1 0 a A × A
48 47 ad6antr A D PsMet X A X v metUnif D u = v A × A w ran a + D -1 0 a w v a + w = D -1 0 a D A × A -1 0 a = D -1 0 a A × A
49 42 48 eqtr4d A D PsMet X A X v metUnif D u = v A × A w ran a + D -1 0 a w v a + w = D -1 0 a w A × A = D A × A -1 0 a
50 rspe a + w A × A = D A × A -1 0 a a + w A × A = D A × A -1 0 a
51 40 49 50 syl2anc A D PsMet X A X v metUnif D u = v A × A w ran a + D -1 0 a w v a + w = D -1 0 a a + w A × A = D A × A -1 0 a
52 vex w V
53 52 inex1 w A × A V
54 eqid a + D A × A -1 0 a = a + D A × A -1 0 a
55 54 elrnmpt w A × A V w A × A ran a + D A × A -1 0 a a + w A × A = D A × A -1 0 a
56 53 55 ax-mp w A × A ran a + D A × A -1 0 a a + w A × A = D A × A -1 0 a
57 51 56 sylibr A D PsMet X A X v metUnif D u = v A × A w ran a + D -1 0 a w v a + w = D -1 0 a w A × A ran a + D A × A -1 0 a
58 simpllr A D PsMet X A X v metUnif D u = v A × A w ran a + D -1 0 a w v a + w = D -1 0 a w v
59 ssinss1 w v w A × A v
60 58 59 syl A D PsMet X A X v metUnif D u = v A × A w ran a + D -1 0 a w v a + w = D -1 0 a w A × A v
61 inss2 w A × A A × A
62 61 a1i A D PsMet X A X v metUnif D u = v A × A w ran a + D -1 0 a w v a + w = D -1 0 a w A × A A × A
63 pweq u = v A × A 𝒫 u = 𝒫 v A × A
64 63 eleq2d u = v A × A w A × A 𝒫 u w A × A 𝒫 v A × A
65 53 elpw w A × A 𝒫 v A × A w A × A v A × A
66 64 65 bitrdi u = v A × A w A × A 𝒫 u w A × A v A × A
67 ssin w A × A v w A × A A × A w A × A v A × A
68 66 67 bitr4di u = v A × A w A × A 𝒫 u w A × A v w A × A A × A
69 68 ad5antlr A D PsMet X A X v metUnif D u = v A × A w ran a + D -1 0 a w v a + w = D -1 0 a w A × A 𝒫 u w A × A v w A × A A × A
70 60 62 69 mpbir2and A D PsMet X A X v metUnif D u = v A × A w ran a + D -1 0 a w v a + w = D -1 0 a w A × A 𝒫 u
71 inelcm w A × A ran a + D A × A -1 0 a w A × A 𝒫 u ran a + D A × A -1 0 a 𝒫 u
72 57 70 71 syl2anc A D PsMet X A X v metUnif D u = v A × A w ran a + D -1 0 a w v a + w = D -1 0 a ran a + D A × A -1 0 a 𝒫 u
73 simplr A D PsMet X A X v metUnif D u = v A × A w ran a + D -1 0 a w v w ran a + D -1 0 a
74 eqid a + D -1 0 a = a + D -1 0 a
75 74 elrnmpt w V w ran a + D -1 0 a a + w = D -1 0 a
76 75 elv w ran a + D -1 0 a a + w = D -1 0 a
77 73 76 sylib A D PsMet X A X v metUnif D u = v A × A w ran a + D -1 0 a w v a + w = D -1 0 a
78 33 39 72 77 r19.29af2 A D PsMet X A X v metUnif D u = v A × A w ran a + D -1 0 a w v ran a + D A × A -1 0 a 𝒫 u
79 ssn0 A X A X
80 79 ancoms A A X X
81 80 3adant2 A D PsMet X A X X
82 metuel X D PsMet X v metUnif D v X × X w ran a + D -1 0 a w v
83 81 43 82 syl2anc A D PsMet X A X v metUnif D v X × X w ran a + D -1 0 a w v
84 83 simplbda A D PsMet X A X v metUnif D w ran a + D -1 0 a w v
85 84 adantr A D PsMet X A X v metUnif D u = v A × A w ran a + D -1 0 a w v
86 78 85 r19.29a A D PsMet X A X v metUnif D u = v A × A ran a + D A × A -1 0 a 𝒫 u
87 86 r19.29an A D PsMet X A X v metUnif D u = v A × A ran a + D A × A -1 0 a 𝒫 u
88 26 87 jca A D PsMet X A X v metUnif D u = v A × A u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u
89 simprl A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u u 𝒫 A × A
90 89 elpwid A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u u A × A
91 simpl3 A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u A X
92 xpss12 A X A X A × A X × X
93 91 91 92 syl2anc A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u A × A X × X
94 90 93 sstrd A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u u X × X
95 difssd A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u X × X A × A X × X
96 94 95 unssd A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u u X × X A × A X × X
97 simplr A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u v 𝒫 u b + v = D A × A -1 0 b b +
98 eqidd A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u v 𝒫 u b + v = D A × A -1 0 b D -1 0 b = D -1 0 b
99 4 imaeq2d a = b D -1 0 a = D -1 0 b
100 99 rspceeqv b + D -1 0 b = D -1 0 b a + D -1 0 b = D -1 0 a
101 97 98 100 syl2anc A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u v 𝒫 u b + v = D A × A -1 0 b a + D -1 0 b = D -1 0 a
102 43 ad4antr A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u v 𝒫 u b + v = D A × A -1 0 b D PsMet X
103 cnvexg D PsMet X D -1 V
104 imaexg D -1 V D -1 0 b V
105 74 elrnmpt D -1 0 b V D -1 0 b ran a + D -1 0 a a + D -1 0 b = D -1 0 a
106 102 103 104 105 4syl A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u v 𝒫 u b + v = D A × A -1 0 b D -1 0 b ran a + D -1 0 a a + D -1 0 b = D -1 0 a
107 101 106 mpbird A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u v 𝒫 u b + v = D A × A -1 0 b D -1 0 b ran a + D -1 0 a
108 cnvimass D -1 0 b dom D
109 108 44 fssdm D PsMet X D -1 0 b X × X
110 102 109 syl A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u v 𝒫 u b + v = D A × A -1 0 b D -1 0 b X × X
111 ssdif0 D -1 0 b X × X D -1 0 b X × X =
112 110 111 sylib A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u v 𝒫 u b + v = D A × A -1 0 b D -1 0 b X × X =
113 0ss u
114 112 113 eqsstrdi A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u v 𝒫 u b + v = D A × A -1 0 b D -1 0 b X × X u
115 respreima Fun D D A × A -1 0 b = D -1 0 b A × A
116 102 44 45 115 4syl A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u v 𝒫 u b + v = D A × A -1 0 b D A × A -1 0 b = D -1 0 b A × A
117 simpr A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u v 𝒫 u b + v = D A × A -1 0 b v = D A × A -1 0 b
118 simpllr A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u v 𝒫 u b + v = D A × A -1 0 b v 𝒫 u
119 118 elpwid A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u v 𝒫 u b + v = D A × A -1 0 b v u
120 117 119 eqsstrrd A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u v 𝒫 u b + v = D A × A -1 0 b D A × A -1 0 b u
121 116 120 eqsstrrd A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u v 𝒫 u b + v = D A × A -1 0 b D -1 0 b A × A u
122 114 121 unssd A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u v 𝒫 u b + v = D A × A -1 0 b D -1 0 b X × X D -1 0 b A × A u
123 ssundif D -1 0 b u X × X A × A D -1 0 b u X × X A × A
124 difcom D -1 0 b u X × X A × A D -1 0 b X × X A × A u
125 difdif2 D -1 0 b X × X A × A = D -1 0 b X × X D -1 0 b A × A
126 125 sseq1i D -1 0 b X × X A × A u D -1 0 b X × X D -1 0 b A × A u
127 123 124 126 3bitri D -1 0 b u X × X A × A D -1 0 b X × X D -1 0 b A × A u
128 122 127 sylibr A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u v 𝒫 u b + v = D A × A -1 0 b D -1 0 b u X × X A × A
129 sseq1 w = D -1 0 b w u X × X A × A D -1 0 b u X × X A × A
130 129 rspcev D -1 0 b ran a + D -1 0 a D -1 0 b u X × X A × A w ran a + D -1 0 a w u X × X A × A
131 107 128 130 syl2anc A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u v 𝒫 u b + v = D A × A -1 0 b w ran a + D -1 0 a w u X × X A × A
132 elin v ran a + D A × A -1 0 a 𝒫 u v ran a + D A × A -1 0 a v 𝒫 u
133 6 elrnmpt v V v ran a + D A × A -1 0 a b + v = D A × A -1 0 b
134 133 elv v ran a + D A × A -1 0 a b + v = D A × A -1 0 b
135 134 anbi1i v ran a + D A × A -1 0 a v 𝒫 u b + v = D A × A -1 0 b v 𝒫 u
136 ancom b + v = D A × A -1 0 b v 𝒫 u v 𝒫 u b + v = D A × A -1 0 b
137 132 135 136 3bitri v ran a + D A × A -1 0 a 𝒫 u v 𝒫 u b + v = D A × A -1 0 b
138 137 exbii v v ran a + D A × A -1 0 a 𝒫 u v v 𝒫 u b + v = D A × A -1 0 b
139 n0 ran a + D A × A -1 0 a 𝒫 u v v ran a + D A × A -1 0 a 𝒫 u
140 df-rex v 𝒫 u b + v = D A × A -1 0 b v v 𝒫 u b + v = D A × A -1 0 b
141 138 139 140 3bitr4i ran a + D A × A -1 0 a 𝒫 u v 𝒫 u b + v = D A × A -1 0 b
142 141 biimpi ran a + D A × A -1 0 a 𝒫 u v 𝒫 u b + v = D A × A -1 0 b
143 142 ad2antll A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u v 𝒫 u b + v = D A × A -1 0 b
144 131 143 r19.29vva A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u w ran a + D -1 0 a w u X × X A × A
145 81 adantr A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u X
146 43 adantr A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u D PsMet X
147 metuel X D PsMet X u X × X A × A metUnif D u X × X A × A X × X w ran a + D -1 0 a w u X × X A × A
148 145 146 147 syl2anc A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u u X × X A × A metUnif D u X × X A × A X × X w ran a + D -1 0 a w u X × X A × A
149 96 144 148 mpbir2and A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u u X × X A × A metUnif D
150 indir u X × X A × A A × A = u A × A X × X A × A A × A
151 disjdifr X × X A × A A × A =
152 151 uneq2i u A × A X × X A × A A × A = u A × A
153 un0 u A × A = u A × A
154 150 152 153 3eqtri u X × X A × A A × A = u A × A
155 df-ss u A × A u A × A = u
156 90 155 sylib A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u u A × A = u
157 154 156 eqtr2id A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u u = u X × X A × A A × A
158 ineq1 v = u X × X A × A v A × A = u X × X A × A A × A
159 158 rspceeqv u X × X A × A metUnif D u = u X × X A × A A × A v metUnif D u = v A × A
160 149 157 159 syl2anc A D PsMet X A X u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u v metUnif D u = v A × A
161 88 160 impbida A D PsMet X A X v metUnif D u = v A × A u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u
162 eqid v metUnif D v A × A = v metUnif D v A × A
163 162 elrnmpt u V u ran v metUnif D v A × A v metUnif D u = v A × A
164 163 elv u ran v metUnif D v A × A v metUnif D u = v A × A
165 pweq v = u 𝒫 v = 𝒫 u
166 165 ineq2d v = u ran a + D A × A -1 0 a 𝒫 v = ran a + D A × A -1 0 a 𝒫 u
167 166 neeq1d v = u ran a + D A × A -1 0 a 𝒫 v ran a + D A × A -1 0 a 𝒫 u
168 167 elrab u v 𝒫 A × A | ran a + D A × A -1 0 a 𝒫 v u 𝒫 A × A ran a + D A × A -1 0 a 𝒫 u
169 161 164 168 3bitr4g A D PsMet X A X u ran v metUnif D v A × A u v 𝒫 A × A | ran a + D A × A -1 0 a 𝒫 v
170 169 eqrdv A D PsMet X A X ran v metUnif D v A × A = v 𝒫 A × A | ran a + D A × A -1 0 a 𝒫 v
171 18 170 eqtrd A D PsMet X A X metUnif D 𝑡 A × A = v 𝒫 A × A | ran a + D A × A -1 0 a 𝒫 v
172 11 13 171 3eqtr4rd A D PsMet X A X metUnif D 𝑡 A × A = metUnif D A × A