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

Theorem metustexhalfOLD 21044
 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 768 . . . 4
2 simplr 755 . . . . . 6
32rphalfcld 11279 . . . . 5
4 eqidd 2444 . . . . 5
5 oveq2 6289 . . . . . . . 8
65imaeq2d 5327 . . . . . . 7
76eqeq2d 2457 . . . . . 6
87rspcev 3196 . . . . 5
93, 4, 8syl2anc 661 . . . 4
10 metust.1 . . . . . . 7
11 oveq2 6289 . . . . . . . . . 10
1211imaeq2d 5327 . . . . . . . . 9
1312cbvmptv 4528 . . . . . . . 8
1413rneqi 5219 . . . . . . 7
1510, 14eqtri 2472 . . . . . 6
1615metustelOLD 21032 . . . . 5
1716biimpar 485 . . . 4
181, 9, 17syl2anc 661 . . 3
19 relco 5495 . . . . 5
2019a1i 11 . . . 4
21 cossxp 5520 . . . . . . . . . 10
22 cnvimass 5347 . . . . . . . . . . . . . 14
23 xmetf 20810 . . . . . . . . . . . . . . 15
24 fdm 5725 . . . . . . . . . . . . . . 15
2523, 24syl 16 . . . . . . . . . . . . . 14
2622, 25syl5sseq 3537 . . . . . . . . . . . . 13
27 dmss 5192 . . . . . . . . . . . . . 14
28 rnss 5221 . . . . . . . . . . . . . 14
29 xpss12 5098 . . . . . . . . . . . . . 14
3027, 28, 29syl2anc 661 . . . . . . . . . . . . 13
3126, 30syl 16 . . . . . . . . . . . 12
3231adantl 466 . . . . . . . . . . 11
33 dmxp 5211 . . . . . . . . . . . . 13
34 rnxp 5427 . . . . . . . . . . . . 13
3533, 34xpeq12d 5014 . . . . . . . . . . . 12
3635adantr 465 . . . . . . . . . . 11
3732, 36sseqtrd 3525 . . . . . . . . . 10
3821, 37syl5ss 3500 . . . . . . . . 9
3938ad3antrrr 729 . . . . . . . 8
4039sselda 3489 . . . . . . 7
41 opelxp 5019 . . . . . . 7
4240, 41sylib 196 . . . . . 6
43 simpll 753 . . . . . . 7
44 simprl 756 . . . . . . 7
45 simprr 757 . . . . . . 7
46 simplr 755 . . . . . . 7
47 simplll 759 . . . . . . . . . . . . . . 15
4847simp1d 1009 . . . . . . . . . . . . . 14
4948, 1syl 16 . . . . . . . . . . . . 13
5048, 2syl 16 . . . . . . . . . . . . 13
5149, 50jca 532 . . . . . . . . . . . 12
5247simp2d 1010 . . . . . . . . . . . 12
5347simp3d 1011 . . . . . . . . . . . 12
5451, 52, 533jca 1177 . . . . . . . . . . 11
55 simplr 755 . . . . . . . . . . 11
56 simprl 756 . . . . . . . . . . 11
57 simprr 757 . . . . . . . . . . 11
58 simpll 753 . . . . . . . . . . . . . . 15
5958simp1d 1009 . . . . . . . . . . . . . 14
6059simpld 459 . . . . . . . . . . . . 13
61 ffun 5723 . . . . . . . . . . . . . 14
6223, 61syl 16 . . . . . . . . . . . . 13
6360, 62syl 16 . . . . . . . . . . . 12
6458simp2d 1010 . . . . . . . . . . . . . 14
6558simp3d 1011 . . . . . . . . . . . . . 14
6664, 65, 41sylanbrc 664 . . . . . . . . . . . . 13
6760, 25syl 16 . . . . . . . . . . . . 13
6866, 67eleqtrrd 2534 . . . . . . . . . . . 12
69 0xr 9643 . . . . . . . . . . . . . 14
7069a1i 11 . . . . . . . . . . . . 13
7159simprd 463 . . . . . . . . . . . . . 14
7271rpxrd 11268 . . . . . . . . . . . . 13
7360, 23syl 16 . . . . . . . . . . . . . 14
7473, 66ffvelrnd 6017 . . . . . . . . . . . . 13
75 xmetge0 20825 . . . . . . . . . . . . . . 15
7660, 64, 65, 75syl3anc 1229 . . . . . . . . . . . . . 14
77 df-ov 6284 . . . . . . . . . . . . . 14
7876, 77syl6breq 4476 . . . . . . . . . . . . 13
7977, 74syl5eqel 2535 . . . . . . . . . . . . . . 15
80 0re 9599 . . . . . . . . . . . . . . . . . . . 20
8180a1i 11 . . . . . . . . . . . . . . . . . . 19
8271rpred 11267 . . . . . . . . . . . . . . . . . . . . 21
8382rehalfcld 10792 . . . . . . . . . . . . . . . . . . . 20
8483rexrd 9646 . . . . . . . . . . . . . . . . . . 19
85 df-ov 6284 . . . . . . . . . . . . . . . . . . . 20
86 simplr 755 . . . . . . . . . . . . . . . . . . . . . . 23
87 opelxp 5019 . . . . . . . . . . . . . . . . . . . . . . 23
8864, 86, 87sylanbrc 664 . . . . . . . . . . . . . . . . . . . . . 22
8988, 67eleqtrrd 2534 . . . . . . . . . . . . . . . . . . . . 21
90 simprl 756 . . . . . . . . . . . . . . . . . . . . . 22
91 df-br 4438 . . . . . . . . . . . . . . . . . . . . . 22
9290, 91sylib 196 . . . . . . . . . . . . . . . . . . . . 21
93 fvimacnv 5987 . . . . . . . . . . . . . . . . . . . . . 22
9493biimpar 485 . . . . . . . . . . . . . . . . . . . . 21
9563, 89, 92, 94syl21anc 1228 . . . . . . . . . . . . . . . . . . . 20
9685, 95syl5eqel 2535 . . . . . . . . . . . . . . . . . . 19
97 elico2 11599 . . . . . . . . . . . . . . . . . . . . 21
9897biimpa 484 . . . . . . . . . . . . . . . . . . . 20
9998simp1d 1009 . . . . . . . . . . . . . . . . . . 19
10081, 84, 96, 99syl21anc 1228 . . . . . . . . . . . . . . . . . 18
101 df-ov 6284 . . . . . . . . . . . . . . . . . . . 20
102 opelxp 5019 . . . . . . . . . . . . . . . . . . . . . . 23
10386, 65, 102sylanbrc 664 . . . . . . . . . . . . . . . . . . . . . 22
104103, 67eleqtrrd 2534 . . . . . . . . . . . . . . . . . . . . 21
105 simprr 757 . . . . . . . . . . . . . . . . . . . . . 22
106 df-br 4438 . . . . . . . . . . . . . . . . . . . . . 22
107105, 106sylib 196 . . . . . . . . . . . . . . . . . . . . 21
108 fvimacnv 5987 . . . . . . . . . . . . . . . . . . . . . 22
109108biimpar 485 . . . . . . . . . . . . . . . . . . . . 21
11063, 104, 107, 109syl21anc 1228 . . . . . . . . . . . . . . . . . . . 20
111101, 110syl5eqel 2535 . . . . . . . . . . . . . . . . . . 19
112 elico2 11599 . . . . . . . . . . . . . . . . . . . . 21
113112biimpa 484 . . . . . . . . . . . . . . . . . . . 20
114113simp1d 1009 . . . . . . . . . . . . . . . . . . 19
11581, 84, 111, 114syl21anc 1228 . . . . . . . . . . . . . . . . . 18
116 rexadd 11442 . . . . . . . . . . . . . . . . . 18
117100, 115, 116syl2anc 661 . . . . . . . . . . . . . . . . 17
118100, 115readdcld 9626 . . . . . . . . . . . . . . . . 17
119117, 118eqeltrd 2531 . . . . . . . . . . . . . . . 16
120119rexrd 9646 . . . . . . . . . . . . . . 15
121 xmettri 20832 . . . . . . . . . . . . . . . 16
12260, 64, 65, 86, 121syl13anc 1231 . . . . . . . . . . . . . . 15
12398simp3d 1011 . . . . . . . . . . . . . . . . . 18
12481, 84, 96, 123syl21anc 1228 . . . . . . . . . . . . . . . . 17
125113simp3d 1011 . . . . . . . . . . . . . . . . . 18
12681, 84, 111, 125syl21anc 1228 . . . . . . . . . . . . . . . . 17
127100, 115, 82, 124, 126lt2halvesd 10793 . . . . . . . . . . . . . . . 16
128117, 127eqbrtrd 4457 . . . . . . . . . . . . . . 15
12979, 120, 72, 122, 128xrlelttrd 11374 . . . . . . . . . . . . . 14
13077, 129syl5eqbrr 4471 . . . . . . . . . . . . 13
131 elico1 11583 . . . . . . . . . . . . . 14
132131biimpar 485 . . . . . . . . . . . . 13
13370, 72, 74, 78, 130, 132syl23anc 1236 . . . . . . . . . . . 12
134 fvimacnv 5987 . . . . . . . . . . . . . 14
135134biimpa 484 . . . . . . . . . . . . 13
136 df-br 4438 . . . . . . . . . . . . 13
137135, 136sylibr 212 . . . . . . . . . . . 12
13863, 68, 133, 137syl21anc 1228 . . . . . . . . . . 11
13954, 55, 56, 57, 138syl22anc 1230 . . . . . . . . . 10
14048simprd 463 . . . . . . . . . . 11
141140breqd 4448 . . . . . . . . . 10
142139, 141mpbird 232 . . . . . . . . 9
143 simpr 461 . . . . . . . . . . . . 13
144 df-br 4438 . . . . . . . . . . . . 13
145143, 144sylibr 212 . . . . . . . . . . . 12
146 vex 3098 . . . . . . . . . . . . 13
147 vex 3098 . . . . . . . . . . . . 13
148146, 147brco 5163 . . . . . . . . . . . 12
149145, 148sylib 196 . . . . . . . . . . 11
15026adantl 466 . . . . . . . . . . . . . . . . . . . . . 22
151150, 28syl 16 . . . . . . . . . . . . . . . . . . . . 21
15234adantr 465 . . . . . . . . . . . . . . . . . . . . 21
153151, 152sseqtrd 3525 . . . . . . . . . . . . . . . . . . . 20
154153adantr 465 . . . . . . . . . . . . . . . . . . 19
155 vex 3098 . . . . . . . . . . . . . . . . . . . . 21
156146, 155brelrn 5223 . . . . . . . . . . . . . . . . . . . 20
157156adantl 466 . . . . . . . . . . . . . . . . . . 19
158154, 157sseldd 3490 . . . . . . . . . . . . . . . . . 18
159158adantrr 716 . . . . . . . . . . . . . . . . 17
160159ex 434 . . . . . . . . . . . . . . . 16
161160ancrd 554 . . . . . . . . . . . . . . 15
162161eximdv 1697 . . . . . . . . . . . . . 14
163162ad3antrrr 729 . . . . . . . . . . . . 13
1641633ad2ant1 1018 . . . . . . . . . . . 12
165164adantr 465 . . . . . . . . . . 11
166149, 165mpd 15 . . . . . . . . . 10
167 df-rex 2799 . . . . . . . . . 10
168166, 167sylibr 212 . . . . . . . . 9
169142, 168r19.29a 2985 . . . . . . . 8
170 df-br 4438 . . . . . . . 8
171169, 170sylib 196 . . . . . . 7
17243, 44, 45, 46, 171syl31anc 1232 . . . . . 6
17342, 172mpdan 668 . . . . 5
174173ex 434 . . . 4
17520, 174relssdv 5085 . . 3
176 id 22 . . . . . 6
177176, 176coeq12d 5157 . . . . 5
178177sseq1d 3516 . . . 4
179178rspcev 3196 . . 3
18018, 175, 179syl2anc 661 . 2
18110metustelOLD 21032 . . . 4