Metamath Proof Explorer


Theorem xrsxmet

Description: The metric on the extended reals is a proper extended metric. (Contributed by Mario Carneiro, 4-Sep-2015)

Ref Expression
Hypothesis xrsxmet.1 D = dist 𝑠 *
Assertion xrsxmet D ∞Met *

Proof

Step Hyp Ref Expression
1 xrsxmet.1 D = dist 𝑠 *
2 xrex * V
3 2 a1i * V
4 id y * y *
5 xnegcl x * x *
6 xaddcl y * x * y + 𝑒 x *
7 4 5 6 syl2anr x * y * y + 𝑒 x *
8 xnegcl y * y *
9 xaddcl x * y * x + 𝑒 y *
10 8 9 sylan2 x * y * x + 𝑒 y *
11 7 10 ifcld x * y * if x y y + 𝑒 x x + 𝑒 y *
12 11 rgen2 x * y * if x y y + 𝑒 x x + 𝑒 y *
13 1 xrsds D = x * , y * if x y y + 𝑒 x x + 𝑒 y
14 13 fmpo x * y * if x y y + 𝑒 x x + 𝑒 y * D : * × * *
15 12 14 mpbi D : * × * *
16 15 a1i D : * × * *
17 breq2 y + 𝑒 x = if x y y + 𝑒 x x + 𝑒 y 0 y + 𝑒 x 0 if x y y + 𝑒 x x + 𝑒 y
18 breq2 x + 𝑒 y = if x y y + 𝑒 x x + 𝑒 y 0 x + 𝑒 y 0 if x y y + 𝑒 x x + 𝑒 y
19 xsubge0 y * x * 0 y + 𝑒 x x y
20 19 ancoms x * y * 0 y + 𝑒 x x y
21 20 biimpar x * y * x y 0 y + 𝑒 x
22 xrletri x * y * x y y x
23 22 orcanai x * y * ¬ x y y x
24 xsubge0 x * y * 0 x + 𝑒 y y x
25 24 biimpar x * y * y x 0 x + 𝑒 y
26 23 25 syldan x * y * ¬ x y 0 x + 𝑒 y
27 17 18 21 26 ifbothda x * y * 0 if x y y + 𝑒 x x + 𝑒 y
28 1 xrsdsval x * y * x D y = if x y y + 𝑒 x x + 𝑒 y
29 27 28 breqtrrd x * y * 0 x D y
30 29 adantl x * y * 0 x D y
31 29 biantrud x * y * x D y 0 x D y 0 0 x D y
32 28 11 eqeltrd x * y * x D y *
33 0xr 0 *
34 xrletri3 x D y * 0 * x D y = 0 x D y 0 0 x D y
35 32 33 34 sylancl x * y * x D y = 0 x D y 0 0 x D y
36 simpr x * y * x D y = 0 x = y x = y
37 simplr x * y * x D y = 0 x y x D y = 0
38 0re 0
39 37 38 eqeltrdi x * y * x D y = 0 x y x D y
40 1 xrsdsreclb x * y * x y x D y x y
41 40 ad4ant124 x * y * x D y = 0 x y x D y x y
42 39 41 mpbid x * y * x D y = 0 x y x y
43 42 simpld x * y * x D y = 0 x y x
44 43 recnd x * y * x D y = 0 x y x
45 42 simprd x * y * x D y = 0 x y y
46 45 recnd x * y * x D y = 0 x y y
47 rexsub x y x + 𝑒 y = x y
48 42 47 syl x * y * x D y = 0 x y x + 𝑒 y = x y
49 28 eqeq1d x * y * x D y = 0 if x y y + 𝑒 x x + 𝑒 y = 0
50 49 biimpa x * y * x D y = 0 if x y y + 𝑒 x x + 𝑒 y = 0
51 50 adantr x * y * x D y = 0 x y if x y y + 𝑒 x x + 𝑒 y = 0
52 xneg11 y + 𝑒 x * 0 * y + 𝑒 x = 0 y + 𝑒 x = 0
53 7 33 52 sylancl x * y * y + 𝑒 x = 0 y + 𝑒 x = 0
54 simpr x * y * y *
55 5 adantr x * y * x *
56 xnegdi y * x * y + 𝑒 x = y + 𝑒 x
57 54 55 56 syl2anc x * y * y + 𝑒 x = y + 𝑒 x
58 xnegneg x * x = x
59 58 adantr x * y * x = x
60 59 oveq2d x * y * y + 𝑒 x = y + 𝑒 x
61 8 adantl x * y * y *
62 simpl x * y * x *
63 xaddcom y * x * y + 𝑒 x = x + 𝑒 y
64 61 62 63 syl2anc x * y * y + 𝑒 x = x + 𝑒 y
65 57 60 64 3eqtrd x * y * y + 𝑒 x = x + 𝑒 y
66 xneg0 0 = 0
67 66 a1i x * y * 0 = 0
68 65 67 eqeq12d x * y * y + 𝑒 x = 0 x + 𝑒 y = 0
69 53 68 bitr3d x * y * y + 𝑒 x = 0 x + 𝑒 y = 0
70 69 ad2antrr x * y * x D y = 0 x y y + 𝑒 x = 0 x + 𝑒 y = 0
71 biidd x * y * x D y = 0 x y x + 𝑒 y = 0 x + 𝑒 y = 0
72 eqeq1 y + 𝑒 x = if x y y + 𝑒 x x + 𝑒 y y + 𝑒 x = 0 if x y y + 𝑒 x x + 𝑒 y = 0
73 72 bibi1d y + 𝑒 x = if x y y + 𝑒 x x + 𝑒 y y + 𝑒 x = 0 x + 𝑒 y = 0 if x y y + 𝑒 x x + 𝑒 y = 0 x + 𝑒 y = 0
74 eqeq1 x + 𝑒 y = if x y y + 𝑒 x x + 𝑒 y x + 𝑒 y = 0 if x y y + 𝑒 x x + 𝑒 y = 0
75 74 bibi1d x + 𝑒 y = if x y y + 𝑒 x x + 𝑒 y x + 𝑒 y = 0 x + 𝑒 y = 0 if x y y + 𝑒 x x + 𝑒 y = 0 x + 𝑒 y = 0
76 73 75 ifboth y + 𝑒 x = 0 x + 𝑒 y = 0 x + 𝑒 y = 0 x + 𝑒 y = 0 if x y y + 𝑒 x x + 𝑒 y = 0 x + 𝑒 y = 0
77 70 71 76 syl2anc x * y * x D y = 0 x y if x y y + 𝑒 x x + 𝑒 y = 0 x + 𝑒 y = 0
78 51 77 mpbid x * y * x D y = 0 x y x + 𝑒 y = 0
79 48 78 eqtr3d x * y * x D y = 0 x y x y = 0
80 44 46 79 subeq0d x * y * x D y = 0 x y x = y
81 36 80 pm2.61dane x * y * x D y = 0 x = y
82 81 ex x * y * x D y = 0 x = y
83 1 xrsdsval y * y * y D y = if y y y + 𝑒 y y + 𝑒 y
84 83 anidms y * y D y = if y y y + 𝑒 y y + 𝑒 y
85 xrleid y * y y
86 85 iftrued y * if y y y + 𝑒 y y + 𝑒 y = y + 𝑒 y
87 xnegid y * y + 𝑒 y = 0
88 84 86 87 3eqtrd y * y D y = 0
89 88 adantl x * y * y D y = 0
90 oveq1 x = y x D y = y D y
91 90 eqeq1d x = y x D y = 0 y D y = 0
92 89 91 syl5ibrcom x * y * x = y x D y = 0
93 82 92 impbid x * y * x D y = 0 x = y
94 31 35 93 3bitr2d x * y * x D y 0 x = y
95 94 adantl x * y * x D y 0 x = y
96 simplrr x * y * z * z D x z D y z = x z D y
97 96 leidd x * y * z * z D x z D y z = x z D y z D y
98 simpr x * y * z * z D x z D y z = x z = x
99 98 oveq1d x * y * z * z D x z D y z = x z D y = x D y
100 98 oveq1d x * y * z * z D x z D y z = x z D x = x D x
101 simpll1 x * y * z * z D x z D y z = x x *
102 oveq12 y = x y = x y D y = x D x
103 102 anidms y = x y D y = x D x
104 103 eqeq1d y = x y D y = 0 x D x = 0
105 104 88 vtoclga x * x D x = 0
106 101 105 syl x * y * z * z D x z D y z = x x D x = 0
107 100 106 eqtrd x * y * z * z D x z D y z = x z D x = 0
108 107 oveq1d x * y * z * z D x z D y z = x z D x + z D y = 0 + z D y
109 96 recnd x * y * z * z D x z D y z = x z D y
110 109 addid2d x * y * z * z D x z D y z = x 0 + z D y = z D y
111 108 110 eqtr2d x * y * z * z D x z D y z = x z D y = z D x + z D y
112 97 99 111 3brtr3d x * y * z * z D x z D y z = x x D y z D x + z D y
113 simpr x * y * z * z D x z D y z = y z = y
114 113 oveq1d x * y * z * z D x z D y z = y z D x = y D x
115 simplrl x * y * z * z D x z D y z = y z D x
116 114 115 eqeltrrd x * y * z * z D x z D y z = y y D x
117 116 leidd x * y * z * z D x z D y z = y y D x y D x
118 simpll1 x * y * z * z D x z D y z = y x *
119 simpll2 x * y * z * z D x z D y z = y y *
120 oveq2 x = y y D x = y D y
121 90 120 eqtr4d x = y x D y = y D x
122 121 adantl x * y * x = y x D y = y D x
123 eqeq2 x + 𝑒 y = if y x x + 𝑒 y y + 𝑒 x if x y y + 𝑒 x x + 𝑒 y = x + 𝑒 y if x y y + 𝑒 x x + 𝑒 y = if y x x + 𝑒 y y + 𝑒 x
124 eqeq2 y + 𝑒 x = if y x x + 𝑒 y y + 𝑒 x if x y y + 𝑒 x x + 𝑒 y = y + 𝑒 x if x y y + 𝑒 x x + 𝑒 y = if y x x + 𝑒 y y + 𝑒 x
125 xrleloe x * y * x y x < y x = y
126 125 adantr x * y * x y x y x < y x = y
127 simpr x * y * x y x y
128 127 neneqd x * y * x y ¬ x = y
129 biorf ¬ x = y x < y x = y x < y
130 orcom x = y x < y x < y x = y
131 129 130 bitrdi ¬ x = y x < y x < y x = y
132 128 131 syl x * y * x y x < y x < y x = y
133 xrltnle x * y * x < y ¬ y x
134 133 adantr x * y * x y x < y ¬ y x
135 126 132 134 3bitr2d x * y * x y x y ¬ y x
136 135 con2bid x * y * x y y x ¬ x y
137 136 biimpa x * y * x y y x ¬ x y
138 137 iffalsed x * y * x y y x if x y y + 𝑒 x x + 𝑒 y = x + 𝑒 y
139 135 biimpar x * y * x y ¬ y x x y
140 139 iftrued x * y * x y ¬ y x if x y y + 𝑒 x x + 𝑒 y = y + 𝑒 x
141 123 124 138 140 ifbothda x * y * x y if x y y + 𝑒 x x + 𝑒 y = if y x x + 𝑒 y y + 𝑒 x
142 28 adantr x * y * x y x D y = if x y y + 𝑒 x x + 𝑒 y
143 1 xrsdsval y * x * y D x = if y x x + 𝑒 y y + 𝑒 x
144 143 ancoms x * y * y D x = if y x x + 𝑒 y y + 𝑒 x
145 144 adantr x * y * x y y D x = if y x x + 𝑒 y y + 𝑒 x
146 141 142 145 3eqtr4d x * y * x y x D y = y D x
147 122 146 pm2.61dane x * y * x D y = y D x
148 118 119 147 syl2anc x * y * z * z D x z D y z = y x D y = y D x
149 113 oveq1d x * y * z * z D x z D y z = y z D y = y D y
150 119 88 syl x * y * z * z D x z D y z = y y D y = 0
151 149 150 eqtrd x * y * z * z D x z D y z = y z D y = 0
152 114 151 oveq12d x * y * z * z D x z D y z = y z D x + z D y = y D x + 0
153 116 recnd x * y * z * z D x z D y z = y y D x
154 153 addid1d x * y * z * z D x z D y z = y y D x + 0 = y D x
155 152 154 eqtrd x * y * z * z D x z D y z = y z D x + z D y = y D x
156 117 148 155 3brtr4d x * y * z * z D x z D y z = y x D y z D x + z D y
157 simplrl x * y * z * z D x z D y z x z y z D x
158 simpll3 x * y * z * z D x z D y z x z y z *
159 simpll1 x * y * z * z D x z D y z x z y x *
160 simprl x * y * z * z D x z D y z x z y z x
161 1 xrsdsreclb z * x * z x z D x z x
162 158 159 160 161 syl3anc x * y * z * z D x z D y z x z y z D x z x
163 157 162 mpbid x * y * z * z D x z D y z x z y z x
164 163 simprd x * y * z * z D x z D y z x z y x
165 164 recnd x * y * z * z D x z D y z x z y x
166 simplrr x * y * z * z D x z D y z x z y z D y
167 simpll2 x * y * z * z D x z D y z x z y y *
168 simprr x * y * z * z D x z D y z x z y z y
169 1 xrsdsreclb z * y * z y z D y z y
170 158 167 168 169 syl3anc x * y * z * z D x z D y z x z y z D y z y
171 166 170 mpbid x * y * z * z D x z D y z x z y z y
172 171 simprd x * y * z * z D x z D y z x z y y
173 172 recnd x * y * z * z D x z D y z x z y y
174 163 simpld x * y * z * z D x z D y z x z y z
175 174 recnd x * y * z * z D x z D y z x z y z
176 165 173 175 abs3difd x * y * z * z D x z D y z x z y x y x z + z y
177 1 xrsdsreval x y x D y = x y
178 164 172 177 syl2anc x * y * z * z D x z D y z x z y x D y = x y
179 1 xrsdsreval z x z D x = z x
180 163 179 syl x * y * z * z D x z D y z x z y z D x = z x
181 175 165 abssubd x * y * z * z D x z D y z x z y z x = x z
182 180 181 eqtrd x * y * z * z D x z D y z x z y z D x = x z
183 1 xrsdsreval z y z D y = z y
184 171 183 syl x * y * z * z D x z D y z x z y z D y = z y
185 182 184 oveq12d x * y * z * z D x z D y z x z y z D x + z D y = x z + z y
186 176 178 185 3brtr4d x * y * z * z D x z D y z x z y x D y z D x + z D y
187 112 156 186 pm2.61da2ne x * y * z * z D x z D y x D y z D x + z D y
188 187 3adant1 x * y * z * z D x z D y x D y z D x + z D y
189 3 16 30 95 188 isxmet2d D ∞Met *
190 189 mptru D ∞Met *