This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐷 = ( dist ‘ ℝ*𝑠 )
Assertion xrsxmet 𝐷 ∈ ( ∞Met ‘ ℝ* )

Proof

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