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∈ℝ→ADB=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∈ℝ*→ADB=ifA≤BB+𝑒−AA+𝑒−B
5 2 3 4 syl2an ⊢A∈ℝ∧B∈ℝ→ADB=ifA≤BB+𝑒−AA+𝑒−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∈ℝ→ifA≤BB+𝑒−AA+𝑒−B=A−B
22 5 21 eqtrd ⊢A∈ℝ∧B∈ℝ→ADB=A−B