Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  restmetu Structured version   Visualization version   Unicode version

Theorem restmetu 21663
 Description: The uniform structure generated by the restriction of a metric is its trace. (Contributed by Thierry Arnoux, 18-Dec-2017.)
Assertion
Ref Expression
restmetu PsMet metUnift metUnif

Proof of Theorem restmetu
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp1 1030 . . . 4 PsMet
2 psmetres2 21408 . . . . 5 PsMet PsMet
323adant1 1048 . . . 4 PsMet PsMet
4 oveq2 6316 . . . . . . . 8
54imaeq2d 5174 . . . . . . 7
65cbvmptv 4488 . . . . . 6
76rneqi 5067 . . . . 5
87metustfbas 21650 . . . 4 PsMet
91, 3, 8syl2anc 673 . . 3 PsMet
10 fgval 20963 . . 3
119, 10syl 17 . 2 PsMet
12 metuval 21642 . . 3 PsMet metUnif
133, 12syl 17 . 2 PsMet metUnif
14 fvex 5889 . . . 4 metUnif
153elfvexd 5907 . . . . 5 PsMet
16 xpexg 6612 . . . . 5
1715, 15, 16syl2anc 673 . . . 4 PsMet
18 restval 15403 . . . 4 metUnif metUnift metUnif
1914, 17, 18sylancr 676 . . 3 PsMet metUnift metUnif
20 inss2 3644 . . . . . . . . . . 11
21 sseq1 3439 . . . . . . . . . . 11
2220, 21mpbiri 241 . . . . . . . . . 10
23 vex 3034 . . . . . . . . . . 11
2423elpw 3948 . . . . . . . . . 10
2522, 24sylibr 217 . . . . . . . . 9
2625rexlimivw 2869 . . . . . . . 8 metUnif
2726adantl 473 . . . . . . 7 PsMet metUnif
28 nfv 1769 . . . . . . . . . . . 12 PsMet metUnif
29 nfmpt1 4485 . . . . . . . . . . . . . 14
3029nfrn 5083 . . . . . . . . . . . . 13
3130nfcri 2606 . . . . . . . . . . . 12
3228, 31nfan 2031 . . . . . . . . . . 11 PsMet metUnif
33 nfv 1769 . . . . . . . . . . 11
3432, 33nfan 2031 . . . . . . . . . 10 PsMet metUnif
35 nfmpt1 4485 . . . . . . . . . . . . 13
3635nfrn 5083 . . . . . . . . . . . 12
37 nfcv 2612 . . . . . . . . . . . 12
3836, 37nfin 3630 . . . . . . . . . . 11
39 nfcv 2612 . . . . . . . . . . 11
4038, 39nfne 2742 . . . . . . . . . 10
41 simplr 770 . . . . . . . . . . . . 13 PsMet metUnif
42 ineq1 3618 . . . . . . . . . . . . . . 15
4342adantl 473 . . . . . . . . . . . . . 14 PsMet metUnif
44 simp2 1031 . . . . . . . . . . . . . . . 16 PsMet PsMet
45 psmetf 21400 . . . . . . . . . . . . . . . 16 PsMet
46 ffun 5742 . . . . . . . . . . . . . . . 16
47 respreima 6024 . . . . . . . . . . . . . . . 16
4844, 45, 46, 474syl 19 . . . . . . . . . . . . . . 15 PsMet
4948ad6antr 750 . . . . . . . . . . . . . 14 PsMet metUnif
5043, 49eqtr4d 2508 . . . . . . . . . . . . 13 PsMet metUnif
51 rspe 2844 . . . . . . . . . . . . 13
5241, 50, 51syl2anc 673 . . . . . . . . . . . 12 PsMet metUnif
53 vex 3034 . . . . . . . . . . . . . 14
5453inex1 4537 . . . . . . . . . . . . 13
55 eqid 2471 . . . . . . . . . . . . . 14
5655elrnmpt 5087 . . . . . . . . . . . . 13
5754, 56ax-mp 5 . . . . . . . . . . . 12
5852, 57sylibr 217 . . . . . . . . . . 11 PsMet metUnif
59 simpllr 777 . . . . . . . . . . . . 13 PsMet metUnif
60 ssinss1 3651 . . . . . . . . . . . . 13
6159, 60syl 17 . . . . . . . . . . . 12 PsMet metUnif
62 inss2 3644 . . . . . . . . . . . . 13
6362a1i 11 . . . . . . . . . . . 12 PsMet metUnif
64 pweq 3945 . . . . . . . . . . . . . . . 16
6564eleq2d 2534 . . . . . . . . . . . . . . 15
6654elpw 3948 . . . . . . . . . . . . . . 15
6765, 66syl6bb 269 . . . . . . . . . . . . . 14
68 ssin 3645 . . . . . . . . . . . . . 14
6967, 68syl6bbr 271 . . . . . . . . . . . . 13
7069ad5antlr 749 . . . . . . . . . . . 12 PsMet metUnif
7161, 63, 70mpbir2and 936 . . . . . . . . . . 11 PsMet metUnif
72 inelcm 3823 . . . . . . . . . . 11
7358, 71, 72syl2anc 673 . . . . . . . . . 10 PsMet metUnif
74 simplr 770 . . . . . . . . . . 11 PsMet metUnif
75 eqid 2471 . . . . . . . . . . . . 13
7675elrnmpt 5087 . . . . . . . . . . . 12
7753, 76ax-mp 5 . . . . . . . . . . 11
7874, 77sylib 201 . . . . . . . . . 10 PsMet metUnif
7934, 40, 73, 78r19.29af2 2915 . . . . . . . . 9 PsMet metUnif
80 ssn0 3770 . . . . . . . . . . . . . 14
8180ancoms 460 . . . . . . . . . . . . 13
82813adant2 1049 . . . . . . . . . . . 12 PsMet
83 metuel 21657 . . . . . . . . . . . 12 PsMet metUnif
8482, 44, 83syl2anc 673 . . . . . . . . . . 11 PsMet metUnif
8584simplbda 636 . . . . . . . . . 10 PsMet metUnif
8685adantr 472 . . . . . . . . 9 PsMet metUnif
8779, 86r19.29a 2918 . . . . . . . 8 PsMet metUnif
8887r19.29an 2917 . . . . . . 7 PsMet metUnif
8927, 88jca 541 . . . . . 6 PsMet metUnif
90 simprl 772 . . . . . . . . . . 11 PsMet
9190elpwid 3952 . . . . . . . . . 10 PsMet
92 simpl3 1035 . . . . . . . . . . 11 PsMet
93 xpss12 4945 . . . . . . . . . . 11
9492, 92, 93syl2anc 673 . . . . . . . . . 10 PsMet
9591, 94sstrd 3428 . . . . . . . . 9 PsMet
96 difssd 3550 . . . . . . . . 9 PsMet
9795, 96unssd 3601 . . . . . . . 8 PsMet
98 simplr 770 . . . . . . . . . . . 12 PsMet
99 eqidd 2472 . . . . . . . . . . . 12 PsMet
1004imaeq2d 5174 . . . . . . . . . . . . . 14
101100eqeq2d 2481 . . . . . . . . . . . . 13
102101rspcev 3136 . . . . . . . . . . . 12
10398, 99, 102syl2anc 673 . . . . . . . . . . 11 PsMet
10444ad4antr 746 . . . . . . . . . . . 12 PsMet PsMet
105 cnvexg 6758 . . . . . . . . . . . 12 PsMet
106 imaexg 6749 . . . . . . . . . . . 12
10775elrnmpt 5087 . . . . . . . . . . . 12
108104, 105, 106, 1074syl 19 . . . . . . . . . . 11 PsMet
109103, 108mpbird 240 . . . . . . . . . 10 PsMet
110 cnvimass 5194 . . . . . . . . . . . . . . . 16
111 fdm 5745 . . . . . . . . . . . . . . . . 17
11245, 111syl 17 . . . . . . . . . . . . . . . 16 PsMet
113110, 112syl5sseq 3466 . . . . . . . . . . . . . . 15 PsMet
114104, 113syl 17 . . . . . . . . . . . . . 14 PsMet
115 ssdif0 3741 . . . . . . . . . . . . . 14
116114, 115sylib 201 . . . . . . . . . . . . 13 PsMet
117 0ss 3766 . . . . . . . . . . . . 13
118116, 117syl6eqss 3468 . . . . . . . . . . . 12 PsMet
119 respreima 6024 . . . . . . . . . . . . . 14
120104, 45, 46, 1194syl 19 . . . . . . . . . . . . 13 PsMet
121 simpr 468 . . . . . . . . . . . . . 14 PsMet
122 simpllr 777 . . . . . . . . . . . . . . 15 PsMet
123122elpwid 3952 . . . . . . . . . . . . . 14 PsMet
124121, 123eqsstr3d 3453 . . . . . . . . . . . . 13 PsMet
125120, 124eqsstr3d 3453 . . . . . . . . . . . 12 PsMet
126118, 125unssd 3601 . . . . . . . . . . 11 PsMet
127 ssundif 3842 . . . . . . . . . . . 12
128 difcom 3843 . . . . . . . . . . . 12
129 difdif2 3691 . . . . . . . . . . . . 13
130129sseq1i 3442 . . . . . . . . . . . 12
131127, 128, 1303bitri 279 . . . . . . . . . . 11
132126, 131sylibr 217 . . . . . . . . . 10 PsMet
133 sseq1 3439 . . . . . . . . . . 11
134133rspcev 3136 . . . . . . . . . 10
135109, 132, 134syl2anc 673 . . . . . . . . 9 PsMet
136 elin 3608 . . . . . . . . . . . . . 14
137 vex 3034 . . . . . . . . . . . . . . . 16
1386elrnmpt 5087 . . . . . . . . . . . . . . . 16
139137, 138ax-mp 5 . . . . . . . . . . . . . . 15
140139anbi1i 709 . . . . . . . . . . . . . 14
141 ancom 457 . . . . . . . . . . . . . 14
142136, 140, 1413bitri 279 . . . . . . . . . . . . 13
143142exbii 1726 . . . . . . . . . . . 12
144 n0 3732 . . . . . . . . . . . 12
145 df-rex 2762 . . . . . . . . . . . 12
146143, 144, 1453bitr4i 285 . . . . . . . . . . 11
147146biimpi 199 . . . . . . . . . 10
148147ad2antll 743 . . . . . . . . 9 PsMet
149135, 148r19.29vva 2920 . . . . . . . 8 PsMet
15082adantr 472 . . . . . . . . 9 PsMet
15144adantr 472 . . . . . . . . 9 PsMet PsMet
152 metuel 21657 . . . . . . . . 9 PsMet metUnif
153150, 151, 152syl2anc 673 . . . . . . . 8 PsMet metUnif
15497, 149, 153mpbir2and 936 . . . . . . 7 PsMet metUnif
155 indir 3682 . . . . . . . . 9
156 incom 3616 . . . . . . . . . . 11
157 disjdif 3830 . . . . . . . . . . 11
158156, 157eqtr3i 2495 . . . . . . . . . 10
159158uneq2i 3576 . . . . . . . . 9
160 un0 3762 . . . . . . . . 9
161155, 159, 1603eqtri 2497 . . . . . . . 8
162 df-ss 3404 . . . . . . . . 9
16391, 162sylib 201 . . . . . . . 8 PsMet
164161, 163syl5req 2518 . . . . . . 7 PsMet
165 ineq1 3618 . . . . . . . . 9
166165eqeq2d 2481 . . . . . . . 8
167166rspcev 3136 . . . . . . 7 metUnif metUnif
168154, 164, 167syl2anc 673 . . . . . 6 PsMet metUnif
16989, 168impbida 850 . . . . 5 PsMet metUnif
170 eqid 2471 . . . . . . 7 metUnif metUnif
171170elrnmpt 5087 . . . . . 6 metUnif metUnif
17223, 171ax-mp 5 . . . . 5 metUnif metUnif
173 pweq 3945 . . . . . . . 8
174173ineq2d 3625 . . . . . . 7
175174neeq1d 2702 . . . . . 6
176175elrab 3184 . . . . 5
177169, 172, 1763bitr4g 296 . . . 4 PsMet metUnif
178177eqrdv 2469 . . 3 PsMet metUnif
17919, 178eqtrd 2505 . 2 PsMet metUnift
18011, 13, 1793eqtr4rd 2516 1 PsMet metUnift metUnif
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 189   wa 376   w3a 1007   wceq 1452  wex 1671   wcel 1904   wne 2641  wrex 2757  crab 2760  cvv 3031   cdif 3387   cun 3388   cin 3389   wss 3390  c0 3722  cpw 3942   cmpt 4454   cxp 4837  ccnv 4838   cdm 4839   crn 4840   cres 4841  cima 4842   wfun 5583  wf 5585  cfv 5589  (class class class)co 6308  cc0 9557  cxr 9692  crp 11325  cico 11662   ↾t crest 15397  PsMetcpsmet 19031  cfbas 19035  cfg 19036  metUnifcmetu 19038 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-po 4760  df-so 4761  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-1st 6812  df-2nd 6813  df-er 7381  df-map 7492  df-en 7588  df-dom 7589  df-sdom 7590  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-rp 11326  df-ico 11666  df-rest 15399  df-psmet 19039  df-fbas 19044  df-fg 19045  df-metu 19046 This theorem is referenced by:  reust  22418  qqhucn  28870
 Copyright terms: Public domain W3C validator