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 ADPsMetXAXmetUnifD𝑡A×A=metUnifDA×A

Proof

Step Hyp Ref Expression
1 simp1 ADPsMetXAXA
2 psmetres2 DPsMetXAXDA×APsMetA
3 2 3adant1 ADPsMetXAXDA×APsMetA
4 oveq2 a=b0a=0b
5 4 imaeq2d a=bDA×A-10a=DA×A-10b
6 5 cbvmptv a+DA×A-10a=b+DA×A-10b
7 6 rneqi rana+DA×A-10a=ranb+DA×A-10b
8 7 metustfbas ADA×APsMetArana+DA×A-10afBasA×A
9 1 3 8 syl2anc ADPsMetXAXrana+DA×A-10afBasA×A
10 fgval rana+DA×A-10afBasA×AA×AfilGenrana+DA×A-10a=v𝒫A×A|rana+DA×A-10a𝒫v
11 9 10 syl ADPsMetXAXA×AfilGenrana+DA×A-10a=v𝒫A×A|rana+DA×A-10a𝒫v
12 metuval DA×APsMetAmetUnifDA×A=A×AfilGenrana+DA×A-10a
13 3 12 syl ADPsMetXAXmetUnifDA×A=A×AfilGenrana+DA×A-10a
14 fvex metUnifDV
15 3 elfvexd ADPsMetXAXAV
16 15 15 xpexd ADPsMetXAXA×AV
17 restval metUnifDVA×AVmetUnifD𝑡A×A=ranvmetUnifDvA×A
18 14 16 17 sylancr ADPsMetXAXmetUnifD𝑡A×A=ranvmetUnifDvA×A
19 inss2 vA×AA×A
20 sseq1 u=vA×AuA×AvA×AA×A
21 19 20 mpbiri u=vA×AuA×A
22 vex uV
23 22 elpw u𝒫A×AuA×A
24 21 23 sylibr u=vA×Au𝒫A×A
25 24 rexlimivw vmetUnifDu=vA×Au𝒫A×A
26 25 adantl ADPsMetXAXvmetUnifDu=vA×Au𝒫A×A
27 nfv aADPsMetXAXvmetUnifDu=vA×A
28 nfmpt1 _aa+D-10a
29 28 nfrn _arana+D-10a
30 29 nfcri awrana+D-10a
31 27 30 nfan aADPsMetXAXvmetUnifDu=vA×Awrana+D-10a
32 nfv awv
33 31 32 nfan aADPsMetXAXvmetUnifDu=vA×Awrana+D-10awv
34 nfmpt1 _aa+DA×A-10a
35 34 nfrn _arana+DA×A-10a
36 nfcv _a𝒫u
37 35 36 nfin _arana+DA×A-10a𝒫u
38 nfcv _a
39 37 38 nfne arana+DA×A-10a𝒫u
40 simplr ADPsMetXAXvmetUnifDu=vA×Awrana+D-10awva+w=D-10aa+
41 ineq1 w=D-10awA×A=D-10aA×A
42 41 adantl ADPsMetXAXvmetUnifDu=vA×Awrana+D-10awva+w=D-10awA×A=D-10aA×A
43 simp2 ADPsMetXAXDPsMetX
44 psmetf DPsMetXD:X×X*
45 ffun D:X×X*FunD
46 respreima FunDDA×A-10a=D-10aA×A
47 43 44 45 46 4syl ADPsMetXAXDA×A-10a=D-10aA×A
48 47 ad6antr ADPsMetXAXvmetUnifDu=vA×Awrana+D-10awva+w=D-10aDA×A-10a=D-10aA×A
49 42 48 eqtr4d ADPsMetXAXvmetUnifDu=vA×Awrana+D-10awva+w=D-10awA×A=DA×A-10a
50 rspe a+wA×A=DA×A-10aa+wA×A=DA×A-10a
51 40 49 50 syl2anc ADPsMetXAXvmetUnifDu=vA×Awrana+D-10awva+w=D-10aa+wA×A=DA×A-10a
52 vex wV
53 52 inex1 wA×AV
54 eqid a+DA×A-10a=a+DA×A-10a
55 54 elrnmpt wA×AVwA×Arana+DA×A-10aa+wA×A=DA×A-10a
56 53 55 ax-mp wA×Arana+DA×A-10aa+wA×A=DA×A-10a
57 51 56 sylibr ADPsMetXAXvmetUnifDu=vA×Awrana+D-10awva+w=D-10awA×Arana+DA×A-10a
58 simpllr ADPsMetXAXvmetUnifDu=vA×Awrana+D-10awva+w=D-10awv
59 ssinss1 wvwA×Av
60 58 59 syl ADPsMetXAXvmetUnifDu=vA×Awrana+D-10awva+w=D-10awA×Av
61 inss2 wA×AA×A
62 61 a1i ADPsMetXAXvmetUnifDu=vA×Awrana+D-10awva+w=D-10awA×AA×A
63 pweq u=vA×A𝒫u=𝒫vA×A
64 63 eleq2d u=vA×AwA×A𝒫uwA×A𝒫vA×A
65 53 elpw wA×A𝒫vA×AwA×AvA×A
66 64 65 bitrdi u=vA×AwA×A𝒫uwA×AvA×A
67 ssin wA×AvwA×AA×AwA×AvA×A
68 66 67 bitr4di u=vA×AwA×A𝒫uwA×AvwA×AA×A
69 68 ad5antlr ADPsMetXAXvmetUnifDu=vA×Awrana+D-10awva+w=D-10awA×A𝒫uwA×AvwA×AA×A
70 60 62 69 mpbir2and ADPsMetXAXvmetUnifDu=vA×Awrana+D-10awva+w=D-10awA×A𝒫u
71 inelcm wA×Arana+DA×A-10awA×A𝒫urana+DA×A-10a𝒫u
72 57 70 71 syl2anc ADPsMetXAXvmetUnifDu=vA×Awrana+D-10awva+w=D-10arana+DA×A-10a𝒫u
73 simplr ADPsMetXAXvmetUnifDu=vA×Awrana+D-10awvwrana+D-10a
74 eqid a+D-10a=a+D-10a
75 74 elrnmpt wVwrana+D-10aa+w=D-10a
76 75 elv wrana+D-10aa+w=D-10a
77 73 76 sylib ADPsMetXAXvmetUnifDu=vA×Awrana+D-10awva+w=D-10a
78 33 39 72 77 r19.29af2 ADPsMetXAXvmetUnifDu=vA×Awrana+D-10awvrana+DA×A-10a𝒫u
79 ssn0 AXAX
80 79 ancoms AAXX
81 80 3adant2 ADPsMetXAXX
82 metuel XDPsMetXvmetUnifDvX×Xwrana+D-10awv
83 81 43 82 syl2anc ADPsMetXAXvmetUnifDvX×Xwrana+D-10awv
84 83 simplbda ADPsMetXAXvmetUnifDwrana+D-10awv
85 84 adantr ADPsMetXAXvmetUnifDu=vA×Awrana+D-10awv
86 78 85 r19.29a ADPsMetXAXvmetUnifDu=vA×Arana+DA×A-10a𝒫u
87 86 r19.29an ADPsMetXAXvmetUnifDu=vA×Arana+DA×A-10a𝒫u
88 26 87 jca ADPsMetXAXvmetUnifDu=vA×Au𝒫A×Arana+DA×A-10a𝒫u
89 simprl ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uu𝒫A×A
90 89 elpwid ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uuA×A
91 simpl3 ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uAX
92 xpss12 AXAXA×AX×X
93 91 91 92 syl2anc ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uA×AX×X
94 90 93 sstrd ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uuX×X
95 difssd ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uX×XA×AX×X
96 94 95 unssd ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uuX×XA×AX×X
97 simplr ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uv𝒫ub+v=DA×A-10bb+
98 eqidd ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uv𝒫ub+v=DA×A-10bD-10b=D-10b
99 4 imaeq2d a=bD-10a=D-10b
100 99 rspceeqv b+D-10b=D-10ba+D-10b=D-10a
101 97 98 100 syl2anc ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uv𝒫ub+v=DA×A-10ba+D-10b=D-10a
102 43 ad4antr ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uv𝒫ub+v=DA×A-10bDPsMetX
103 cnvexg DPsMetXD-1V
104 imaexg D-1VD-10bV
105 74 elrnmpt D-10bVD-10brana+D-10aa+D-10b=D-10a
106 102 103 104 105 4syl ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uv𝒫ub+v=DA×A-10bD-10brana+D-10aa+D-10b=D-10a
107 101 106 mpbird ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uv𝒫ub+v=DA×A-10bD-10brana+D-10a
108 cnvimass D-10bdomD
109 108 44 fssdm DPsMetXD-10bX×X
110 102 109 syl ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uv𝒫ub+v=DA×A-10bD-10bX×X
111 ssdif0 D-10bX×XD-10bX×X=
112 110 111 sylib ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uv𝒫ub+v=DA×A-10bD-10bX×X=
113 0ss u
114 112 113 eqsstrdi ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uv𝒫ub+v=DA×A-10bD-10bX×Xu
115 respreima FunDDA×A-10b=D-10bA×A
116 102 44 45 115 4syl ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uv𝒫ub+v=DA×A-10bDA×A-10b=D-10bA×A
117 simpr ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uv𝒫ub+v=DA×A-10bv=DA×A-10b
118 simpllr ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uv𝒫ub+v=DA×A-10bv𝒫u
119 118 elpwid ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uv𝒫ub+v=DA×A-10bvu
120 117 119 eqsstrrd ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uv𝒫ub+v=DA×A-10bDA×A-10bu
121 116 120 eqsstrrd ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uv𝒫ub+v=DA×A-10bD-10bA×Au
122 114 121 unssd ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uv𝒫ub+v=DA×A-10bD-10bX×XD-10bA×Au
123 ssundif D-10buX×XA×AD-10buX×XA×A
124 difcom D-10buX×XA×AD-10bX×XA×Au
125 difdif2 D-10bX×XA×A=D-10bX×XD-10bA×A
126 125 sseq1i D-10bX×XA×AuD-10bX×XD-10bA×Au
127 123 124 126 3bitri D-10buX×XA×AD-10bX×XD-10bA×Au
128 122 127 sylibr ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uv𝒫ub+v=DA×A-10bD-10buX×XA×A
129 sseq1 w=D-10bwuX×XA×AD-10buX×XA×A
130 129 rspcev D-10brana+D-10aD-10buX×XA×Awrana+D-10awuX×XA×A
131 107 128 130 syl2anc ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uv𝒫ub+v=DA×A-10bwrana+D-10awuX×XA×A
132 elin vrana+DA×A-10a𝒫uvrana+DA×A-10av𝒫u
133 6 elrnmpt vVvrana+DA×A-10ab+v=DA×A-10b
134 133 elv vrana+DA×A-10ab+v=DA×A-10b
135 134 anbi1i vrana+DA×A-10av𝒫ub+v=DA×A-10bv𝒫u
136 ancom b+v=DA×A-10bv𝒫uv𝒫ub+v=DA×A-10b
137 132 135 136 3bitri vrana+DA×A-10a𝒫uv𝒫ub+v=DA×A-10b
138 137 exbii vvrana+DA×A-10a𝒫uvv𝒫ub+v=DA×A-10b
139 n0 rana+DA×A-10a𝒫uvvrana+DA×A-10a𝒫u
140 df-rex v𝒫ub+v=DA×A-10bvv𝒫ub+v=DA×A-10b
141 138 139 140 3bitr4i rana+DA×A-10a𝒫uv𝒫ub+v=DA×A-10b
142 141 biimpi rana+DA×A-10a𝒫uv𝒫ub+v=DA×A-10b
143 142 ad2antll ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uv𝒫ub+v=DA×A-10b
144 131 143 r19.29vva ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uwrana+D-10awuX×XA×A
145 81 adantr ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uX
146 43 adantr ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uDPsMetX
147 metuel XDPsMetXuX×XA×AmetUnifDuX×XA×AX×Xwrana+D-10awuX×XA×A
148 145 146 147 syl2anc ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uuX×XA×AmetUnifDuX×XA×AX×Xwrana+D-10awuX×XA×A
149 96 144 148 mpbir2and ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uuX×XA×AmetUnifD
150 indir uX×XA×AA×A=uA×AX×XA×AA×A
151 disjdifr X×XA×AA×A=
152 151 uneq2i uA×AX×XA×AA×A=uA×A
153 un0 uA×A=uA×A
154 150 152 153 3eqtri uX×XA×AA×A=uA×A
155 df-ss uA×AuA×A=u
156 90 155 sylib ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uuA×A=u
157 154 156 eqtr2id ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uu=uX×XA×AA×A
158 ineq1 v=uX×XA×AvA×A=uX×XA×AA×A
159 158 rspceeqv uX×XA×AmetUnifDu=uX×XA×AA×AvmetUnifDu=vA×A
160 149 157 159 syl2anc ADPsMetXAXu𝒫A×Arana+DA×A-10a𝒫uvmetUnifDu=vA×A
161 88 160 impbida ADPsMetXAXvmetUnifDu=vA×Au𝒫A×Arana+DA×A-10a𝒫u
162 eqid vmetUnifDvA×A=vmetUnifDvA×A
163 162 elrnmpt uVuranvmetUnifDvA×AvmetUnifDu=vA×A
164 163 elv uranvmetUnifDvA×AvmetUnifDu=vA×A
165 pweq v=u𝒫v=𝒫u
166 165 ineq2d v=urana+DA×A-10a𝒫v=rana+DA×A-10a𝒫u
167 166 neeq1d v=urana+DA×A-10a𝒫vrana+DA×A-10a𝒫u
168 167 elrab uv𝒫A×A|rana+DA×A-10a𝒫vu𝒫A×Arana+DA×A-10a𝒫u
169 161 164 168 3bitr4g ADPsMetXAXuranvmetUnifDvA×Auv𝒫A×A|rana+DA×A-10a𝒫v
170 169 eqrdv ADPsMetXAXranvmetUnifDvA×A=v𝒫A×A|rana+DA×A-10a𝒫v
171 18 170 eqtrd ADPsMetXAXmetUnifD𝑡A×A=v𝒫A×A|rana+DA×A-10a𝒫v
172 11 13 171 3eqtr4rd ADPsMetXAXmetUnifD𝑡A×A=metUnifDA×A