Metamath Proof Explorer


Theorem metustexhalf

Description: For any element A of the filter base generated by the metric D , 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)

Ref Expression
Hypothesis metust.1 F = ran a + D -1 0 a
Assertion metustexhalf X D PsMet X A F v F v v A

Proof

Step Hyp Ref Expression
1 metust.1 F = ran a + D -1 0 a
2 simp-4r X D PsMet X A F a + A = D -1 0 a D PsMet X
3 simplr X D PsMet X A F a + A = D -1 0 a a +
4 3 rphalfcld X D PsMet X A F a + A = D -1 0 a a 2 +
5 eqidd X D PsMet X A F a + A = D -1 0 a D -1 0 a 2 = D -1 0 a 2
6 oveq2 b = a 2 0 b = 0 a 2
7 6 imaeq2d b = a 2 D -1 0 b = D -1 0 a 2
8 7 rspceeqv a 2 + D -1 0 a 2 = D -1 0 a 2 b + D -1 0 a 2 = D -1 0 b
9 4 5 8 syl2anc X D PsMet X A F a + A = D -1 0 a b + D -1 0 a 2 = D -1 0 b
10 oveq2 a = b 0 a = 0 b
11 10 imaeq2d a = b D -1 0 a = D -1 0 b
12 11 cbvmptv a + D -1 0 a = b + D -1 0 b
13 12 rneqi ran a + D -1 0 a = ran b + D -1 0 b
14 1 13 eqtri F = ran b + D -1 0 b
15 14 metustel D PsMet X D -1 0 a 2 F b + D -1 0 a 2 = D -1 0 b
16 15 biimpar D PsMet X b + D -1 0 a 2 = D -1 0 b D -1 0 a 2 F
17 2 9 16 syl2anc X D PsMet X A F a + A = D -1 0 a D -1 0 a 2 F
18 relco Rel D -1 0 a 2 D -1 0 a 2
19 18 a1i X D PsMet X A F a + A = D -1 0 a Rel D -1 0 a 2 D -1 0 a 2
20 cossxp D -1 0 a 2 D -1 0 a 2 dom D -1 0 a 2 × ran D -1 0 a 2
21 cnvimass D -1 0 a 2 dom D
22 psmetf D PsMet X D : X × X *
23 21 22 fssdm D PsMet X D -1 0 a 2 X × X
24 dmss D -1 0 a 2 X × X dom D -1 0 a 2 dom X × X
25 rnss D -1 0 a 2 X × X ran D -1 0 a 2 ran X × X
26 xpss12 dom D -1 0 a 2 dom X × X ran D -1 0 a 2 ran X × X dom D -1 0 a 2 × ran D -1 0 a 2 dom X × X × ran X × X
27 24 25 26 syl2anc D -1 0 a 2 X × X dom D -1 0 a 2 × ran D -1 0 a 2 dom X × X × ran X × X
28 23 27 syl D PsMet X dom D -1 0 a 2 × ran D -1 0 a 2 dom X × X × ran X × X
29 28 adantl X D PsMet X dom D -1 0 a 2 × ran D -1 0 a 2 dom X × X × ran X × X
30 dmxp X dom X × X = X
31 rnxp X ran X × X = X
32 30 31 xpeq12d X dom X × X × ran X × X = X × X
33 32 adantr X D PsMet X dom X × X × ran X × X = X × X
34 29 33 sseqtrd X D PsMet X dom D -1 0 a 2 × ran D -1 0 a 2 X × X
35 20 34 sstrid X D PsMet X D -1 0 a 2 D -1 0 a 2 X × X
36 35 ad3antrrr X D PsMet X A F a + A = D -1 0 a D -1 0 a 2 D -1 0 a 2 X × X
37 36 sselda X D PsMet X A F a + A = D -1 0 a p q D -1 0 a 2 D -1 0 a 2 p q X × X
38 opelxp p q X × X p X q X
39 37 38 sylib X D PsMet X A F a + A = D -1 0 a p q D -1 0 a 2 D -1 0 a 2 p X q X
40 simpll X D PsMet X A F a + A = D -1 0 a p q D -1 0 a 2 D -1 0 a 2 p X q X X D PsMet X A F a + A = D -1 0 a
41 simprl X D PsMet X A F a + A = D -1 0 a p q D -1 0 a 2 D -1 0 a 2 p X q X p X
42 simprr X D PsMet X A F a + A = D -1 0 a p q D -1 0 a 2 D -1 0 a 2 p X q X q X
43 simplr X D PsMet X A F a + A = D -1 0 a p q D -1 0 a 2 D -1 0 a 2 p X q X p q D -1 0 a 2 D -1 0 a 2
44 simplll X D PsMet X A F a + A = D -1 0 a p X q X p q D -1 0 a 2 D -1 0 a 2 r X p D -1 0 a 2 r r D -1 0 a 2 q X D PsMet X A F a + A = D -1 0 a p X q X
45 44 simp1d X D PsMet X A F a + A = D -1 0 a p X q X p q D -1 0 a 2 D -1 0 a 2 r X p D -1 0 a 2 r r D -1 0 a 2 q X D PsMet X A F a + A = D -1 0 a
46 45 2 syl X D PsMet X A F a + A = D -1 0 a p X q X p q D -1 0 a 2 D -1 0 a 2 r X p D -1 0 a 2 r r D -1 0 a 2 q D PsMet X
47 45 3 syl X D PsMet X A F a + A = D -1 0 a p X q X p q D -1 0 a 2 D -1 0 a 2 r X p D -1 0 a 2 r r D -1 0 a 2 q a +
48 46 47 jca X D PsMet X A F a + A = D -1 0 a p X q X p q D -1 0 a 2 D -1 0 a 2 r X p D -1 0 a 2 r r D -1 0 a 2 q D PsMet X a +
49 44 simp2d X D PsMet X A F a + A = D -1 0 a p X q X p q D -1 0 a 2 D -1 0 a 2 r X p D -1 0 a 2 r r D -1 0 a 2 q p X
50 44 simp3d X D PsMet X A F a + A = D -1 0 a p X q X p q D -1 0 a 2 D -1 0 a 2 r X p D -1 0 a 2 r r D -1 0 a 2 q q X
51 48 49 50 3jca X D PsMet X A F a + A = D -1 0 a p X q X p q D -1 0 a 2 D -1 0 a 2 r X p D -1 0 a 2 r r D -1 0 a 2 q D PsMet X a + p X q X
52 simplr X D PsMet X A F a + A = D -1 0 a p X q X p q D -1 0 a 2 D -1 0 a 2 r X p D -1 0 a 2 r r D -1 0 a 2 q r X
53 simprl X D PsMet X A F a + A = D -1 0 a p X q X p q D -1 0 a 2 D -1 0 a 2 r X p D -1 0 a 2 r r D -1 0 a 2 q p D -1 0 a 2 r
54 simprr X D PsMet X A F a + A = D -1 0 a p X q X p q D -1 0 a 2 D -1 0 a 2 r X p D -1 0 a 2 r r D -1 0 a 2 q r D -1 0 a 2 q
55 simpll D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q D PsMet X a + p X q X
56 55 simp1d D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q D PsMet X a +
57 56 simpld D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q D PsMet X
58 22 ffund D PsMet X Fun D
59 57 58 syl D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q Fun D
60 55 simp2d D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q p X
61 55 simp3d D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q q X
62 60 61 opelxpd D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q p q X × X
63 22 fdmd D PsMet X dom D = X × X
64 57 63 syl D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q dom D = X × X
65 62 64 eleqtrrd D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q p q dom D
66 0xr 0 *
67 66 a1i D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q 0 *
68 56 simprd D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q a +
69 68 rpxrd D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q a *
70 57 22 syl D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q D : X × X *
71 70 62 ffvelrnd D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q D p q *
72 psmetge0 D PsMet X p X q X 0 p D q
73 57 60 61 72 syl3anc D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q 0 p D q
74 df-ov p D q = D p q
75 73 74 breqtrdi D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q 0 D p q
76 74 71 eqeltrid D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q p D q *
77 0red D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q 0
78 68 rpred D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q a
79 78 rehalfcld D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q a 2
80 79 rexrd D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q a 2 *
81 df-ov p D r = D p r
82 simplr D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q r X
83 60 82 opelxpd D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q p r X × X
84 83 64 eleqtrrd D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q p r dom D
85 simprl D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q p D -1 0 a 2 r
86 df-br p D -1 0 a 2 r p r D -1 0 a 2
87 85 86 sylib D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q p r D -1 0 a 2
88 fvimacnv Fun D p r dom D D p r 0 a 2 p r D -1 0 a 2
89 88 biimpar Fun D p r dom D p r D -1 0 a 2 D p r 0 a 2
90 59 84 87 89 syl21anc D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q D p r 0 a 2
91 81 90 eqeltrid D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q p D r 0 a 2
92 elico2 0 a 2 * p D r 0 a 2 p D r 0 p D r p D r < a 2
93 92 biimpa 0 a 2 * p D r 0 a 2 p D r 0 p D r p D r < a 2
94 93 simp1d 0 a 2 * p D r 0 a 2 p D r
95 77 80 91 94 syl21anc D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q p D r
96 df-ov r D q = D r q
97 82 61 opelxpd D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q r q X × X
98 97 64 eleqtrrd D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q r q dom D
99 simprr D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q r D -1 0 a 2 q
100 df-br r D -1 0 a 2 q r q D -1 0 a 2
101 99 100 sylib D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q r q D -1 0 a 2
102 fvimacnv Fun D r q dom D D r q 0 a 2 r q D -1 0 a 2
103 102 biimpar Fun D r q dom D r q D -1 0 a 2 D r q 0 a 2
104 59 98 101 103 syl21anc D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q D r q 0 a 2
105 96 104 eqeltrid D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q r D q 0 a 2
106 elico2 0 a 2 * r D q 0 a 2 r D q 0 r D q r D q < a 2
107 106 biimpa 0 a 2 * r D q 0 a 2 r D q 0 r D q r D q < a 2
108 107 simp1d 0 a 2 * r D q 0 a 2 r D q
109 77 80 105 108 syl21anc D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q r D q
110 95 109 rexaddd D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q p D r + 𝑒 r D q = p D r + r D q
111 95 109 readdcld D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q p D r + r D q
112 110 111 eqeltrd D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q p D r + 𝑒 r D q
113 112 rexrd D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q p D r + 𝑒 r D q *
114 psmettri D PsMet X p X q X r X p D q p D r + 𝑒 r D q
115 57 60 61 82 114 syl13anc D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q p D q p D r + 𝑒 r D q
116 93 simp3d 0 a 2 * p D r 0 a 2 p D r < a 2
117 77 80 91 116 syl21anc D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q p D r < a 2
118 107 simp3d 0 a 2 * r D q 0 a 2 r D q < a 2
119 77 80 105 118 syl21anc D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q r D q < a 2
120 95 109 78 117 119 lt2halvesd D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q p D r + r D q < a
121 110 120 eqbrtrd D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q p D r + 𝑒 r D q < a
122 76 113 69 115 121 xrlelttrd D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q p D q < a
123 74 122 eqbrtrrid D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q D p q < a
124 67 69 71 75 123 elicod D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q D p q 0 a
125 fvimacnv Fun D p q dom D D p q 0 a p q D -1 0 a
126 125 biimpa Fun D p q dom D D p q 0 a p q D -1 0 a
127 df-br p D -1 0 a q p q D -1 0 a
128 126 127 sylibr Fun D p q dom D D p q 0 a p D -1 0 a q
129 59 65 124 128 syl21anc D PsMet X a + p X q X r X p D -1 0 a 2 r r D -1 0 a 2 q p D -1 0 a q
130 51 52 53 54 129 syl22anc X D PsMet X A F a + A = D -1 0 a p X q X p q D -1 0 a 2 D -1 0 a 2 r X p D -1 0 a 2 r r D -1 0 a 2 q p D -1 0 a q
131 45 simprd X D PsMet X A F a + A = D -1 0 a p X q X p q D -1 0 a 2 D -1 0 a 2 r X p D -1 0 a 2 r r D -1 0 a 2 q A = D -1 0 a
132 131 breqd X D PsMet X A F a + A = D -1 0 a p X q X p q D -1 0 a 2 D -1 0 a 2 r X p D -1 0 a 2 r r D -1 0 a 2 q p A q p D -1 0 a q
133 130 132 mpbird X D PsMet X A F a + A = D -1 0 a p X q X p q D -1 0 a 2 D -1 0 a 2 r X p D -1 0 a 2 r r D -1 0 a 2 q p A q
134 simpr X D PsMet X A F a + A = D -1 0 a p X q X p q D -1 0 a 2 D -1 0 a 2 p q D -1 0 a 2 D -1 0 a 2
135 df-br p D -1 0 a 2 D -1 0 a 2 q p q D -1 0 a 2 D -1 0 a 2
136 134 135 sylibr X D PsMet X A F a + A = D -1 0 a p X q X p q D -1 0 a 2 D -1 0 a 2 p D -1 0 a 2 D -1 0 a 2 q
137 vex p V
138 vex q V
139 137 138 brco p D -1 0 a 2 D -1 0 a 2 q r p D -1 0 a 2 r r D -1 0 a 2 q
140 136 139 sylib X D PsMet X A F a + A = D -1 0 a p X q X p q D -1 0 a 2 D -1 0 a 2 r p D -1 0 a 2 r r D -1 0 a 2 q
141 23 adantl X D PsMet X D -1 0 a 2 X × X
142 141 25 syl X D PsMet X ran D -1 0 a 2 ran X × X
143 31 adantr X D PsMet X ran X × X = X
144 142 143 sseqtrd X D PsMet X ran D -1 0 a 2 X
145 144 adantr X D PsMet X p D -1 0 a 2 r ran D -1 0 a 2 X
146 vex r V
147 137 146 brelrn p D -1 0 a 2 r r ran D -1 0 a 2
148 147 adantl X D PsMet X p D -1 0 a 2 r r ran D -1 0 a 2
149 145 148 sseldd X D PsMet X p D -1 0 a 2 r r X
150 149 adantrr X D PsMet X p D -1 0 a 2 r r D -1 0 a 2 q r X
151 150 ex X D PsMet X p D -1 0 a 2 r r D -1 0 a 2 q r X
152 151 ancrd X D PsMet X p D -1 0 a 2 r r D -1 0 a 2 q r X p D -1 0 a 2 r r D -1 0 a 2 q
153 152 eximdv X D PsMet X r p D -1 0 a 2 r r D -1 0 a 2 q r r X p D -1 0 a 2 r r D -1 0 a 2 q
154 153 ad3antrrr X D PsMet X A F a + A = D -1 0 a r p D -1 0 a 2 r r D -1 0 a 2 q r r X p D -1 0 a 2 r r D -1 0 a 2 q
155 154 3ad2ant1 X D PsMet X A F a + A = D -1 0 a p X q X r p D -1 0 a 2 r r D -1 0 a 2 q r r X p D -1 0 a 2 r r D -1 0 a 2 q
156 155 adantr X D PsMet X A F a + A = D -1 0 a p X q X p q D -1 0 a 2 D -1 0 a 2 r p D -1 0 a 2 r r D -1 0 a 2 q r r X p D -1 0 a 2 r r D -1 0 a 2 q
157 140 156 mpd X D PsMet X A F a + A = D -1 0 a p X q X p q D -1 0 a 2 D -1 0 a 2 r r X p D -1 0 a 2 r r D -1 0 a 2 q
158 df-rex r X p D -1 0 a 2 r r D -1 0 a 2 q r r X p D -1 0 a 2 r r D -1 0 a 2 q
159 157 158 sylibr X D PsMet X A F a + A = D -1 0 a p X q X p q D -1 0 a 2 D -1 0 a 2 r X p D -1 0 a 2 r r D -1 0 a 2 q
160 133 159 r19.29a X D PsMet X A F a + A = D -1 0 a p X q X p q D -1 0 a 2 D -1 0 a 2 p A q
161 df-br p A q p q A
162 160 161 sylib X D PsMet X A F a + A = D -1 0 a p X q X p q D -1 0 a 2 D -1 0 a 2 p q A
163 40 41 42 43 162 syl31anc X D PsMet X A F a + A = D -1 0 a p q D -1 0 a 2 D -1 0 a 2 p X q X p q A
164 39 163 mpdan X D PsMet X A F a + A = D -1 0 a p q D -1 0 a 2 D -1 0 a 2 p q A
165 164 ex X D PsMet X A F a + A = D -1 0 a p q D -1 0 a 2 D -1 0 a 2 p q A
166 19 165 relssdv X D PsMet X A F a + A = D -1 0 a D -1 0 a 2 D -1 0 a 2 A
167 id v = D -1 0 a 2 v = D -1 0 a 2
168 167 167 coeq12d v = D -1 0 a 2 v v = D -1 0 a 2 D -1 0 a 2
169 168 sseq1d v = D -1 0 a 2 v v A D -1 0 a 2 D -1 0 a 2 A
170 169 rspcev D -1 0 a 2 F D -1 0 a 2 D -1 0 a 2 A v F v v A
171 17 166 170 syl2anc X D PsMet X A F a + A = D -1 0 a v F v v A
172 1 metustel D PsMet X A F a + A = D -1 0 a
173 172 adantl X D PsMet X A F a + A = D -1 0 a
174 173 biimpa X D PsMet X A F a + A = D -1 0 a
175 171 174 r19.29a X D PsMet X A F v F v v A