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	⊢ 𝐷 = ( dist ‘ ℝ^*_𝑠 )
	Assertion	xrsdsreval	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 𝐷 𝐵 ) = ( abs ‘ ( 𝐴 − 𝐵 ) ) )

Proof

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

Metamath Proof Explorer

Theorem xrsdsreval

Proof