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 ( 𝐴 ≤ 𝐵 , ( 𝐵 +𝑒 -𝑒 𝐴 ) , ( 𝐴 +𝑒 -𝑒 𝐵 ) ) )