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

Metamath Proof Explorer

Theorem xrsdsval

Description: The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypothesis xrsds.d ⊢ D = dist ⁡ ℝ 𝑠 *
Assertion xrsdsval ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A D B = if A ≤ B B + 𝑒 − A A + 𝑒 − B

Proof

Step Hyp Ref Expression
1 xrsds.d ⊢ D = dist ⁡ ℝ 𝑠 *
2 breq12 ⊢ x = A ∧ y = B → x ≤ y ↔ A ≤ B
3 id ⊢ y = B → y = B
4 xnegeq ⊢ x = A → − x = − A
5 3 4 oveqan12rd ⊢ x = A ∧ y = B → y + 𝑒 − x = B + 𝑒 − A
6 id ⊢ x = A → x = A
7 xnegeq ⊢ y = B → − y = − B
8 6 7 oveqan12d ⊢ x = A ∧ y = B → x + 𝑒 − y = A + 𝑒 − B
9 2 5 8 ifbieq12d ⊢ x = A ∧ y = B → if x ≤ y y + 𝑒 − x x + 𝑒 − y = if A ≤ B B + 𝑒 − A A + 𝑒 − B
10 1 xrsds ⊢ D = x ∈ ℝ * , y ∈ ℝ * ⟼ if x ≤ y y + 𝑒 − x x + 𝑒 − y
11 ovex ⊢ B + 𝑒 − A ∈ V
12 ovex ⊢ A + 𝑒 − B ∈ V
13 11 12 ifex ⊢ if A ≤ B B + 𝑒 − A A + 𝑒 − B ∈ V
14 9 10 13 ovmpoa ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A D B = if A ≤ B B + 𝑒 − A A + 𝑒 − B