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

Theorem metustexhalf 18596
 Description: For any element of the filter base generated by the metric , the half element (corresponding to half the distance) is also in this base. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
Hypothesis
Ref Expression
metust.1
Assertion
Ref Expression
metustexhalf PsMet
Distinct variable groups:   ,   ,   ,   ,,   ,   ,   ,   ,

Proof of Theorem metustexhalf
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp-4r 745 . . . 4 PsMet PsMet
2 simplr 733 . . . . . 6 PsMet
32rphalfcld 10662 . . . . 5 PsMet
4 eqidd 2439 . . . . 5 PsMet
5 oveq2 6091 . . . . . . . 8
65imaeq2d 5205 . . . . . . 7
76eqeq2d 2449 . . . . . 6
87rspcev 3054 . . . . 5
93, 4, 8syl2anc 644 . . . 4 PsMet
10 metust.1 . . . . . . 7
11 oveq2 6091 . . . . . . . . . 10
1211imaeq2d 5205 . . . . . . . . 9
1312cbvmptv 4302 . . . . . . . 8
1413rneqi 5098 . . . . . . 7
1510, 14eqtri 2458 . . . . . 6
1615metustel 18584 . . . . 5 PsMet
1716biimpar 473 . . . 4 PsMet
181, 9, 17syl2anc 644 . . 3 PsMet
19 relco 5370 . . . . 5
2019a1i 11 . . . 4 PsMet
21 cossxp 5394 . . . . . . . . . 10
22 cnvimass 5226 . . . . . . . . . . . . . 14
23 psmetf 18339 . . . . . . . . . . . . . . 15 PsMet
24 fdm 5597 . . . . . . . . . . . . . . 15
2523, 24syl 16 . . . . . . . . . . . . . 14 PsMet
2622, 25syl5sseq 3398 . . . . . . . . . . . . 13 PsMet
27 dmss 5071 . . . . . . . . . . . . . 14
28 rnss 5100 . . . . . . . . . . . . . 14
29 xpss12 4983 . . . . . . . . . . . . . 14
3027, 28, 29syl2anc 644 . . . . . . . . . . . . 13
3126, 30syl 16 . . . . . . . . . . . 12 PsMet
3231adantl 454 . . . . . . . . . . 11 PsMet
33 dmxp 5090 . . . . . . . . . . . . 13
34 rnxp 5301 . . . . . . . . . . . . 13
3533, 34xpeq12d 4905 . . . . . . . . . . . 12
3635adantr 453 . . . . . . . . . . 11 PsMet
3732, 36sseqtrd 3386 . . . . . . . . . 10 PsMet
3821, 37syl5ss 3361 . . . . . . . . 9 PsMet
3938ad3antrrr 712 . . . . . . . 8 PsMet
4039sselda 3350 . . . . . . 7 PsMet
41 opelxp 4910 . . . . . . 7
4240, 41sylib 190 . . . . . 6 PsMet
43 simpll 732 . . . . . . 7 PsMet PsMet
44 simprl 734 . . . . . . 7 PsMet
45 simprr 735 . . . . . . 7 PsMet
46 simplr 733 . . . . . . 7 PsMet
47 simplll 736 . . . . . . . . . . . . . . 15 PsMet PsMet
4847simp1d 970 . . . . . . . . . . . . . 14 PsMet PsMet
4948, 1syl 16 . . . . . . . . . . . . 13 PsMet PsMet
5048, 2syl 16 . . . . . . . . . . . . 13 PsMet
5149, 50jca 520 . . . . . . . . . . . 12 PsMet PsMet
5247simp2d 971 . . . . . . . . . . . 12 PsMet
5347simp3d 972 . . . . . . . . . . . 12 PsMet
5451, 52, 533jca 1135 . . . . . . . . . . 11 PsMet PsMet
55 simplr 733 . . . . . . . . . . 11 PsMet
56 simprl 734 . . . . . . . . . . 11 PsMet
57 simprr 735 . . . . . . . . . . 11 PsMet
58 simpll 732 . . . . . . . . . . . . . . 15 PsMet PsMet
5958simp1d 970 . . . . . . . . . . . . . 14 PsMet PsMet
6059simpld 447 . . . . . . . . . . . . 13 PsMet PsMet
61 ffun 5595 . . . . . . . . . . . . . 14
6223, 61syl 16 . . . . . . . . . . . . 13 PsMet
6360, 62syl 16 . . . . . . . . . . . 12 PsMet
6458simp2d 971 . . . . . . . . . . . . . 14 PsMet
6558simp3d 972 . . . . . . . . . . . . . 14 PsMet
6664, 65, 41sylanbrc 647 . . . . . . . . . . . . 13 PsMet
6760, 25syl 16 . . . . . . . . . . . . 13 PsMet
6866, 67eleqtrrd 2515 . . . . . . . . . . . 12 PsMet
69 0xr 9133 . . . . . . . . . . . . . 14
7069a1i 11 . . . . . . . . . . . . 13 PsMet
7159simprd 451 . . . . . . . . . . . . . 14 PsMet
7271rpxrd 10651 . . . . . . . . . . . . 13 PsMet
7360, 23syl 16 . . . . . . . . . . . . . 14 PsMet
7473, 66ffvelrnd 5873 . . . . . . . . . . . . 13 PsMet
75 psmetge0 18345 . . . . . . . . . . . . . . 15 PsMet
7660, 64, 65, 75syl3anc 1185 . . . . . . . . . . . . . 14 PsMet
77 df-ov 6086 . . . . . . . . . . . . . 14
7876, 77syl6breq 4253 . . . . . . . . . . . . 13 PsMet
7977, 74syl5eqel 2522 . . . . . . . . . . . . . . 15 PsMet
80 0re 9093 . . . . . . . . . . . . . . . . . . . 20
8180a1i 11 . . . . . . . . . . . . . . . . . . 19 PsMet
8271rpred 10650 . . . . . . . . . . . . . . . . . . . . 21 PsMet
8382rehalfcld 10216 . . . . . . . . . . . . . . . . . . . 20 PsMet
8483rexrd 9136 . . . . . . . . . . . . . . . . . . 19 PsMet
85 df-ov 6086 . . . . . . . . . . . . . . . . . . . 20
86 simplr 733 . . . . . . . . . . . . . . . . . . . . . . 23 PsMet
87 opelxp 4910 . . . . . . . . . . . . . . . . . . . . . . 23
8864, 86, 87sylanbrc 647 . . . . . . . . . . . . . . . . . . . . . 22 PsMet
8988, 67eleqtrrd 2515 . . . . . . . . . . . . . . . . . . . . 21 PsMet
90 simprl 734 . . . . . . . . . . . . . . . . . . . . . 22 PsMet
91 df-br 4215 . . . . . . . . . . . . . . . . . . . . . 22
9290, 91sylib 190 . . . . . . . . . . . . . . . . . . . . 21 PsMet
93 fvimacnv 5847 . . . . . . . . . . . . . . . . . . . . . 22
9493biimpar 473 . . . . . . . . . . . . . . . . . . . . 21
9563, 89, 92, 94syl21anc 1184 . . . . . . . . . . . . . . . . . . . 20 PsMet
9685, 95syl5eqel 2522 . . . . . . . . . . . . . . . . . . 19 PsMet
97 elico2 10976 . . . . . . . . . . . . . . . . . . . . 21
9897biimpa 472 . . . . . . . . . . . . . . . . . . . 20
9998simp1d 970 . . . . . . . . . . . . . . . . . . 19
10081, 84, 96, 99syl21anc 1184 . . . . . . . . . . . . . . . . . 18 PsMet
101 df-ov 6086 . . . . . . . . . . . . . . . . . . . 20
102 opelxp 4910 . . . . . . . . . . . . . . . . . . . . . . 23
10386, 65, 102sylanbrc 647 . . . . . . . . . . . . . . . . . . . . . 22 PsMet
104103, 67eleqtrrd 2515 . . . . . . . . . . . . . . . . . . . . 21 PsMet
105 simprr 735 . . . . . . . . . . . . . . . . . . . . . 22 PsMet
106 df-br 4215 . . . . . . . . . . . . . . . . . . . . . 22
107105, 106sylib 190 . . . . . . . . . . . . . . . . . . . . 21 PsMet
108 fvimacnv 5847 . . . . . . . . . . . . . . . . . . . . . 22
109108biimpar 473 . . . . . . . . . . . . . . . . . . . . 21
11063, 104, 107, 109syl21anc 1184 . . . . . . . . . . . . . . . . . . . 20 PsMet
111101, 110syl5eqel 2522 . . . . . . . . . . . . . . . . . . 19 PsMet
112 elico2 10976 . . . . . . . . . . . . . . . . . . . . 21
113112biimpa 472 . . . . . . . . . . . . . . . . . . . 20
114113simp1d 970 . . . . . . . . . . . . . . . . . . 19
11581, 84, 111, 114syl21anc 1184 . . . . . . . . . . . . . . . . . 18 PsMet
116 rexadd 10820 . . . . . . . . . . . . . . . . . 18
117100, 115, 116syl2anc 644 . . . . . . . . . . . . . . . . 17 PsMet
118100, 115readdcld 9117 . . . . . . . . . . . . . . . . 17 PsMet
119117, 118eqeltrd 2512 . . . . . . . . . . . . . . . 16 PsMet
120119rexrd 9136 . . . . . . . . . . . . . . 15 PsMet
121 psmettri 18344 . . . . . . . . . . . . . . . 16 PsMet
12260, 64, 65, 86, 121syl13anc 1187 . . . . . . . . . . . . . . 15 PsMet
12398simp3d 972 . . . . . . . . . . . . . . . . . 18
12481, 84, 96, 123syl21anc 1184 . . . . . . . . . . . . . . . . 17 PsMet
125113simp3d 972 . . . . . . . . . . . . . . . . . 18
12681, 84, 111, 125syl21anc 1184 . . . . . . . . . . . . . . . . 17 PsMet
127100, 115, 82, 124, 126lt2halvesd 10217 . . . . . . . . . . . . . . . 16 PsMet
128117, 127eqbrtrd 4234 . . . . . . . . . . . . . . 15 PsMet
12979, 120, 72, 122, 128xrlelttrd 10752 . . . . . . . . . . . . . 14 PsMet
13077, 129syl5eqbrr 4248 . . . . . . . . . . . . 13 PsMet
131 elico1 10961 . . . . . . . . . . . . . 14
132131biimpar 473 . . . . . . . . . . . . 13
13370, 72, 74, 78, 130, 132syl23anc 1192 . . . . . . . . . . . 12 PsMet
134 fvimacnv 5847 . . . . . . . . . . . . . 14
135134biimpa 472 . . . . . . . . . . . . 13
136 df-br 4215 . . . . . . . . . . . . 13
137135, 136sylibr 205 . . . . . . . . . . . 12
13863, 68, 133, 137syl21anc 1184 . . . . . . . . . . 11 PsMet
13954, 55, 56, 57, 138syl22anc 1186 . . . . . . . . . 10 PsMet
14048simprd 451 . . . . . . . . . . 11 PsMet
141140breqd 4225 . . . . . . . . . 10 PsMet
142139, 141mpbird 225 . . . . . . . . 9 PsMet
143 simpr 449 . . . . . . . . . . . . 13 PsMet
144 df-br 4215 . . . . . . . . . . . . 13
145143, 144sylibr 205 . . . . . . . . . . . 12 PsMet
146 vex 2961 . . . . . . . . . . . . 13
147 vex 2961 . . . . . . . . . . . . 13
148146, 147brco 5045 . . . . . . . . . . . 12
149145, 148sylib 190 . . . . . . . . . . 11 PsMet
15026adantl 454 . . . . . . . . . . . . . . . . . . . . . 22 PsMet
151150, 28syl 16 . . . . . . . . . . . . . . . . . . . . 21 PsMet
15234adantr 453 . . . . . . . . . . . . . . . . . . . . 21 PsMet
153151, 152sseqtrd 3386 . . . . . . . . . . . . . . . . . . . 20 PsMet
154153adantr 453 . . . . . . . . . . . . . . . . . . 19 PsMet
155 vex 2961 . . . . . . . . . . . . . . . . . . . . 21
156146, 155brelrn 5102 . . . . . . . . . . . . . . . . . . . 20
157156adantl 454 . . . . . . . . . . . . . . . . . . 19 PsMet
158154, 157sseldd 3351 . . . . . . . . . . . . . . . . . 18 PsMet
159158adantrr 699 . . . . . . . . . . . . . . . . 17 PsMet
160159ex 425 . . . . . . . . . . . . . . . 16 PsMet
161160ancrd 539 . . . . . . . . . . . . . . 15 PsMet
162161eximdv 1633 . . . . . . . . . . . . . 14 PsMet
163162ad3antrrr 712 . . . . . . . . . . . . 13 PsMet
1641633ad2ant1 979 . . . . . . . . . . . 12 PsMet
165164adantr 453 . . . . . . . . . . 11 PsMet
166149, 165mpd 15 . . . . . . . . . 10 PsMet
167 df-rex 2713 . . . . . . . . . 10
168166, 167sylibr 205 . . . . . . . . 9 PsMet
169142, 168r19.29a 2852 . . . . . . . 8 PsMet
170 df-br 4215 . . . . . . . 8
171169, 170sylib 190 . . . . . . 7 PsMet
17243, 44, 45, 46, 171syl31anc 1188 . . . . . 6 PsMet
17342, 172mpdan 651 . . . . 5 PsMet
174173ex 425 . . . 4 PsMet
17520, 174relssdv 4970 . . 3 PsMet
176 id 21 . . . . . 6
177176, 176coeq12d 5039 . . . . 5
178177sseq1d 3377 . . . 4
179178rspcev 3054 . . 3
18018, 175, 179syl2anc 644 . 2 PsMet
18110metustel 18584 . . . 4 PsMet
182181adantl 454 . . 3 PsMet
183182biimpa 472 . 2 PsMet
184180, 183r19.29a 2852 1 PsMet
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wa 360   w3a 937  wex 1551   wceq 1653   wcel 1726   wne 2601  wrex 2708   wss 3322  c0 3630  cop 3819   class class class wbr 4214   cmpt 4268   cxp 4878  ccnv 4879   cdm 4880   crn 4881  cima 4883   ccom 4884   wrel 4885   wfun 5450  wf 5452  cfv 5456  (class class class)co 6083  cr 8991  cc0 8992   caddc 8995  cxr 9121   clt 9122   cle 9123   cdiv 9679  c2 10051  crp 10614  cxad 10710  cico 10920  PsMetcpsmet 16687 This theorem is referenced by:  metust  18600 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405  ax-un 4703  ax-cnex 9048  ax-resscn 9049  ax-1cn 9050  ax-icn 9051  ax-addcl 9052  ax-addrcl 9053  ax-mulcl 9054  ax-mulrcl 9055  ax-mulcom 9056  ax-addass 9057  ax-mulass 9058  ax-distr 9059  ax-i2m1 9060  ax-1ne0 9061  ax-1rid 9062  ax-rnegex 9063  ax-rrecex 9064  ax-cnre 9065  ax-pre-lttri 9066  ax-pre-lttrn 9067  ax-pre-ltadd 9068  ax-pre-mulgt0 9069 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-iun 4097  df-br 4215  df-opab 4269  df-mpt 4270  df-id 4500  df-po 4505  df-so 4506  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-f1 5461  df-fo 5462  df-f1o 5463  df-fv 5464  df-ov 6086  df-oprab 6087  df-mpt2 6088  df-1st 6351  df-2nd 6352  df-riota 6551  df-er 6907  df-map 7022  df-en 7112  df-dom 7113  df-sdom 7114  df-pnf 9124  df-mnf 9125  df-xr 9126  df-ltxr 9127  df-le 9128  df-sub 9295  df-neg 9296  df-div 9680  df-2 10060  df-rp 10615  df-xneg 10712  df-xadd 10713  df-xmul 10714  df-ico 10924  df-psmet 16696
 Copyright terms: Public domain W3C validator