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 ` RR*s )
Assertion xrsxmet 
|- D e. ( *Met ` RR* )

Proof

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