Metamath Proof Explorer

Theorem xrsdsreval

Description: The metric of the extended real number structure coincides with the real number metric on the reals. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypothesis xrsds.d ⊢ D = dist ⁡ ℝ 𝑠 *
Assertion xrsdsreval ⊢ A ∈ ℝ ∧ B ∈ ℝ → A D B = A − B

Proof

Step Hyp Ref Expression
1 xrsds.d ⊢ D = dist ⁡ ℝ 𝑠 *
2 rexr ⊢ A ∈ ℝ → A ∈ ℝ *
3 rexr ⊢ B ∈ ℝ → B ∈ ℝ *
4 1 xrsdsval ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A D B = if A ≤ B B + 𝑒 − A A + 𝑒 − B
5 2 3 4 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → A D B = if A ≤ B B + 𝑒 − A A + 𝑒 − B
6 rexsub ⊢ B ∈ ℝ ∧ A ∈ ℝ → B + 𝑒 − A = B − A
7 6 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ → B + 𝑒 − A = B − A
8 7 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → B + 𝑒 − A = B − A
9 abssuble0 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A − B = B − A
10 9 3expa ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A − B = B − A
11 8 10 eqtr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → B + 𝑒 − A = A − B
12 rexsub ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + 𝑒 − B = A − B
13 12 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ ¬ A ≤ B → A + 𝑒 − B = A − B
14 letric ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ∨ B ≤ A
15 14 orcanai ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ ¬ A ≤ B → B ≤ A
16 abssubge0 ⊢ B ∈ ℝ ∧ A ∈ ℝ ∧ B ≤ A → A − B = A − B
17 16 3com12 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≤ A → A − B = A − B
18 17 3expa ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≤ A → A − B = A − B
19 15 18 syldan ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ ¬ A ≤ B → A − B = A − B
20 13 19 eqtr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ ¬ A ≤ B → A + 𝑒 − B = A − B
21 11 20 ifeqda ⊢ A ∈ ℝ ∧ B ∈ ℝ → if A ≤ B B + 𝑒 − A A + 𝑒 − B = A − B
22 5 21 eqtrd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A D B = A − B