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

Theorem metustexhalfOLD 20113
 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.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
metust.1
Assertion
Ref Expression
metustexhalfOLD
Distinct variable groups:   ,   ,   ,   ,,   ,   ,   ,   ,

Proof of Theorem metustexhalfOLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp-4r 766 . . . 4
2 simplr 754 . . . . . 6
32rphalfcld 11031 . . . . 5
4 eqidd 2439 . . . . 5
5 oveq2 6094 . . . . . . . 8
65imaeq2d 5164 . . . . . . 7
76eqeq2d 2449 . . . . . 6
87rspcev 3068 . . . . 5
93, 4, 8syl2anc 661 . . . 4
10 metust.1 . . . . . . 7
11 oveq2 6094 . . . . . . . . . 10
1211imaeq2d 5164 . . . . . . . . 9
1312cbvmptv 4378 . . . . . . . 8
1413rneqi 5061 . . . . . . 7
1510, 14eqtri 2458 . . . . . 6
1615metustelOLD 20101 . . . . 5
1716biimpar 485 . . . 4
181, 9, 17syl2anc 661 . . 3
19 relco 5331 . . . . 5
2019a1i 11 . . . 4
21 cossxp 5355 . . . . . . . . . 10
22 cnvimass 5184 . . . . . . . . . . . . . 14
23 xmetf 19879 . . . . . . . . . . . . . . 15
24 fdm 5558 . . . . . . . . . . . . . . 15
2523, 24syl 16 . . . . . . . . . . . . . 14
2622, 25syl5sseq 3399 . . . . . . . . . . . . 13
27 dmss 5034 . . . . . . . . . . . . . 14
28 rnss 5063 . . . . . . . . . . . . . 14
29 xpss12 4940 . . . . . . . . . . . . . 14
3027, 28, 29syl2anc 661 . . . . . . . . . . . . 13
3126, 30syl 16 . . . . . . . . . . . 12
3231adantl 466 . . . . . . . . . . 11
33 dmxp 5053 . . . . . . . . . . . . 13
34 rnxp 5263 . . . . . . . . . . . . 13
3533, 34xpeq12d 4860 . . . . . . . . . . . 12
3635adantr 465 . . . . . . . . . . 11
3732, 36sseqtrd 3387 . . . . . . . . . 10
3821, 37syl5ss 3362 . . . . . . . . 9
3938ad3antrrr 729 . . . . . . . 8
4039sselda 3351 . . . . . . 7
41 opelxp 4864 . . . . . . 7
4240, 41sylib 196 . . . . . 6
43 simpll 753 . . . . . . 7
44 simprl 755 . . . . . . 7
45 simprr 756 . . . . . . 7
46 simplr 754 . . . . . . 7
47 simplll 757 . . . . . . . . . . . . . . 15
4847simp1d 1000 . . . . . . . . . . . . . 14
4948, 1syl 16 . . . . . . . . . . . . 13
5048, 2syl 16 . . . . . . . . . . . . 13
5149, 50jca 532 . . . . . . . . . . . 12
5247simp2d 1001 . . . . . . . . . . . 12
5347simp3d 1002 . . . . . . . . . . . 12
5451, 52, 533jca 1168 . . . . . . . . . . 11
55 simplr 754 . . . . . . . . . . 11
56 simprl 755 . . . . . . . . . . 11
57 simprr 756 . . . . . . . . . . 11
58 simpll 753 . . . . . . . . . . . . . . 15
5958simp1d 1000 . . . . . . . . . . . . . 14
6059simpld 459 . . . . . . . . . . . . 13
61 ffun 5556 . . . . . . . . . . . . . 14
6223, 61syl 16 . . . . . . . . . . . . 13
6360, 62syl 16 . . . . . . . . . . . 12
6458simp2d 1001 . . . . . . . . . . . . . 14
6558simp3d 1002 . . . . . . . . . . . . . 14
6664, 65, 41sylanbrc 664 . . . . . . . . . . . . 13
6760, 25syl 16 . . . . . . . . . . . . 13
6866, 67eleqtrrd 2515 . . . . . . . . . . . 12
69 0xr 9422 . . . . . . . . . . . . . 14
7069a1i 11 . . . . . . . . . . . . 13
7159simprd 463 . . . . . . . . . . . . . 14
7271rpxrd 11020 . . . . . . . . . . . . 13
7360, 23syl 16 . . . . . . . . . . . . . 14
7473, 66ffvelrnd 5839 . . . . . . . . . . . . 13
75 xmetge0 19894 . . . . . . . . . . . . . . 15
7660, 64, 65, 75syl3anc 1218 . . . . . . . . . . . . . 14
77 df-ov 6089 . . . . . . . . . . . . . 14
7876, 77syl6breq 4326 . . . . . . . . . . . . 13
7977, 74syl5eqel 2522 . . . . . . . . . . . . . . 15
80 0re 9378 . . . . . . . . . . . . . . . . . . . 20
8180a1i 11 . . . . . . . . . . . . . . . . . . 19
8271rpred 11019 . . . . . . . . . . . . . . . . . . . . 21
8382rehalfcld 10563 . . . . . . . . . . . . . . . . . . . 20
8483rexrd 9425 . . . . . . . . . . . . . . . . . . 19
85 df-ov 6089 . . . . . . . . . . . . . . . . . . . 20
86 simplr 754 . . . . . . . . . . . . . . . . . . . . . . 23
87 opelxp 4864 . . . . . . . . . . . . . . . . . . . . . . 23
8864, 86, 87sylanbrc 664 . . . . . . . . . . . . . . . . . . . . . 22
8988, 67eleqtrrd 2515 . . . . . . . . . . . . . . . . . . . . 21
90 simprl 755 . . . . . . . . . . . . . . . . . . . . . 22
91 df-br 4288 . . . . . . . . . . . . . . . . . . . . . 22
9290, 91sylib 196 . . . . . . . . . . . . . . . . . . . . 21
93 fvimacnv 5813 . . . . . . . . . . . . . . . . . . . . . 22
9493biimpar 485 . . . . . . . . . . . . . . . . . . . . 21
9563, 89, 92, 94syl21anc 1217 . . . . . . . . . . . . . . . . . . . 20
9685, 95syl5eqel 2522 . . . . . . . . . . . . . . . . . . 19
97 elico2 11351 . . . . . . . . . . . . . . . . . . . . 21
9897biimpa 484 . . . . . . . . . . . . . . . . . . . 20
9998simp1d 1000 . . . . . . . . . . . . . . . . . . 19
10081, 84, 96, 99syl21anc 1217 . . . . . . . . . . . . . . . . . 18
101 df-ov 6089 . . . . . . . . . . . . . . . . . . . 20
102 opelxp 4864 . . . . . . . . . . . . . . . . . . . . . . 23
10386, 65, 102sylanbrc 664 . . . . . . . . . . . . . . . . . . . . . 22
104103, 67eleqtrrd 2515 . . . . . . . . . . . . . . . . . . . . 21
105 simprr 756 . . . . . . . . . . . . . . . . . . . . . 22
106 df-br 4288 . . . . . . . . . . . . . . . . . . . . . 22
107105, 106sylib 196 . . . . . . . . . . . . . . . . . . . . 21
108 fvimacnv 5813 . . . . . . . . . . . . . . . . . . . . . 22
109108biimpar 485 . . . . . . . . . . . . . . . . . . . . 21
11063, 104, 107, 109syl21anc 1217 . . . . . . . . . . . . . . . . . . . 20
111101, 110syl5eqel 2522 . . . . . . . . . . . . . . . . . . 19
112 elico2 11351 . . . . . . . . . . . . . . . . . . . . 21
113112biimpa 484 . . . . . . . . . . . . . . . . . . . 20
114113simp1d 1000 . . . . . . . . . . . . . . . . . . 19
11581, 84, 111, 114syl21anc 1217 . . . . . . . . . . . . . . . . . 18
116 rexadd 11194 . . . . . . . . . . . . . . . . . 18
117100, 115, 116syl2anc 661 . . . . . . . . . . . . . . . . 17
118100, 115readdcld 9405 . . . . . . . . . . . . . . . . 17
119117, 118eqeltrd 2512 . . . . . . . . . . . . . . . 16
120119rexrd 9425 . . . . . . . . . . . . . . 15
121 xmettri 19901 . . . . . . . . . . . . . . . 16
12260, 64, 65, 86, 121syl13anc 1220 . . . . . . . . . . . . . . 15
12398simp3d 1002 . . . . . . . . . . . . . . . . . 18
12481, 84, 96, 123syl21anc 1217 . . . . . . . . . . . . . . . . 17
125113simp3d 1002 . . . . . . . . . . . . . . . . . 18
12681, 84, 111, 125syl21anc 1217 . . . . . . . . . . . . . . . . 17
127100, 115, 82, 124, 126lt2halvesd 10564 . . . . . . . . . . . . . . . 16
128117, 127eqbrtrd 4307 . . . . . . . . . . . . . . 15
12979, 120, 72, 122, 128xrlelttrd 11126 . . . . . . . . . . . . . 14
13077, 129syl5eqbrr 4321 . . . . . . . . . . . . 13
131 elico1 11335 . . . . . . . . . . . . . 14
132131biimpar 485 . . . . . . . . . . . . 13
13370, 72, 74, 78, 130, 132syl23anc 1225 . . . . . . . . . . . 12
134 fvimacnv 5813 . . . . . . . . . . . . . 14
135134biimpa 484 . . . . . . . . . . . . 13
136 df-br 4288 . . . . . . . . . . . . 13
137135, 136sylibr 212 . . . . . . . . . . . 12
13863, 68, 133, 137syl21anc 1217 . . . . . . . . . . 11
13954, 55, 56, 57, 138syl22anc 1219 . . . . . . . . . 10
14048simprd 463 . . . . . . . . . . 11
141140breqd 4298 . . . . . . . . . 10
142139, 141mpbird 232 . . . . . . . . 9
143 simpr 461 . . . . . . . . . . . . 13
144 df-br 4288 . . . . . . . . . . . . 13
145143, 144sylibr 212 . . . . . . . . . . . 12
146 vex 2970 . . . . . . . . . . . . 13
147 vex 2970 . . . . . . . . . . . . 13
148146, 147brco 5005 . . . . . . . . . . . 12
149145, 148sylib 196 . . . . . . . . . . 11
15026adantl 466 . . . . . . . . . . . . . . . . . . . . . 22
151150, 28syl 16 . . . . . . . . . . . . . . . . . . . . 21
15234adantr 465 . . . . . . . . . . . . . . . . . . . . 21
153151, 152sseqtrd 3387 . . . . . . . . . . . . . . . . . . . 20
154153adantr 465 . . . . . . . . . . . . . . . . . . 19
155 vex 2970 . . . . . . . . . . . . . . . . . . . . 21
156146, 155brelrn 5065 . . . . . . . . . . . . . . . . . . . 20
157156adantl 466 . . . . . . . . . . . . . . . . . . 19
158154, 157sseldd 3352 . . . . . . . . . . . . . . . . . 18
159158adantrr 716 . . . . . . . . . . . . . . . . 17
160159ex 434 . . . . . . . . . . . . . . . 16
161160ancrd 554 . . . . . . . . . . . . . . 15
162161eximdv 1676 . . . . . . . . . . . . . 14
163162ad3antrrr 729 . . . . . . . . . . . . 13
1641633ad2ant1 1009 . . . . . . . . . . . 12
165164adantr 465 . . . . . . . . . . 11
166149, 165mpd 15 . . . . . . . . . 10
167 df-rex 2716 . . . . . . . . . 10
168166, 167sylibr 212 . . . . . . . . 9
169142, 168r19.29a 2857 . . . . . . . 8
170 df-br 4288 . . . . . . . 8
171169, 170sylib 196 . . . . . . 7
17243, 44, 45, 46, 171syl31anc 1221 . . . . . 6
17342, 172mpdan 668 . . . . 5
174173ex 434 . . . 4
17520, 174relssdv 4927 . . 3
176 id 22 . . . . . 6
177176, 176coeq12d 4999 . . . . 5
178177sseq1d 3378 . . . 4
179178rspcev 3068 . . 3
18018, 175, 179syl2anc 661 . 2
18110metustelOLD 20101 . . . 4
182181adantl 466 . . 3
183182biimpa 484 . 2
184180, 183r19.29a 2857 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   w3a 965   wceq 1369  wex 1586   wcel 1756   wne 2601  wrex 2711   wss 3323  c0 3632  cop 3878   class class class wbr 4287   cmpt 4345   cxp 4833  ccnv 4834   cdm 4835   crn 4836  cima 4838   ccom 4839   wrel 4840   wfun 5407  wf 5409  cfv 5413  (class class class)co 6086  cr 9273  cc0 9274   caddc 9277  cxr 9409   clt 9410   cle 9411   cdiv 9985  c2 10363  crp 10983  cxad 11079  cico 11294  cxmt 17776 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-reu 2717  df-rmo 2718  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-po 4636  df-so 4637  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-1st 6572  df-2nd 6573  df-er 7093  df-map 7208  df-en 7303  df-dom 7304  df-sdom 7305  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-div 9986  df-2 10372  df-rp 10984  df-xneg 11081  df-xadd 11082  df-xmul 11083  df-ico 11298  df-xmet 17785 This theorem is referenced by:  metustOLD  20117
 Copyright terms: Public domain W3C validator