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 ⊢ 𝐷 = ( dist ‘ ℝ*𝑠 )
Assertion xrsdsval ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 𝐷 𝐵 ) = if ( 𝐴 ≤ 𝐵 , ( 𝐵 +𝑒 -𝑒 𝐴 ) , ( 𝐴 +𝑒 -𝑒 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 xrsds.d ⊢ 𝐷 = ( dist ‘ ℝ*𝑠 )
2 breq12 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 ≤ 𝑦 ↔ 𝐴 ≤ 𝐵 ) )
3 id ⊢ ( 𝑦 = 𝐵 → 𝑦 = 𝐵 )
4 xnegeq ⊢ ( 𝑥 = 𝐴 → -𝑒 𝑥 = -𝑒 𝐴 )
5 3 4 oveqan12rd ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑦 +𝑒 -𝑒 𝑥 ) = ( 𝐵 +𝑒 -𝑒 𝐴 ) )
6 id ⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
7 xnegeq ⊢ ( 𝑦 = 𝐵 → -𝑒 𝑦 = -𝑒 𝐵 )
8 6 7 oveqan12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 +𝑒 -𝑒 𝑦 ) = ( 𝐴 +𝑒 -𝑒 𝐵 ) )
9 2 5 8 ifbieq12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) = if ( 𝐴 ≤ 𝐵 , ( 𝐵 +𝑒 -𝑒 𝐴 ) , ( 𝐴 +𝑒 -𝑒 𝐵 ) ) )
10 1 xrsds ⊢ 𝐷 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) )
11 ovex ⊢ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ V
12 ovex ⊢ ( 𝐴 +𝑒 -𝑒 𝐵 ) ∈ V
13 11 12 ifex ⊢ if ( 𝐴 ≤ 𝐵 , ( 𝐵 +𝑒 -𝑒 𝐴 ) , ( 𝐴 +𝑒 -𝑒 𝐵 ) ) ∈ V
14 9 10 13 ovmpoa ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 𝐷 𝐵 ) = if ( 𝐴 ≤ 𝐵 , ( 𝐵 +𝑒 -𝑒 𝐴 ) , ( 𝐴 +𝑒 -𝑒 𝐵 ) ) )