Theorem remetdval

Description: Value of the distance function of the metric space of real numbers. (Contributed by NM, 16-May-2007)

	Ref	Expression
Hypothesis	remet.1	⊢ 𝐷 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
Assertion	remetdval	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 𝐷 𝐵 ) = ( abs ‘ ( 𝐴 − 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		remet.1	⊢ 𝐷 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
2		df-ov	⊢ ( 𝐴 𝐷 𝐵 ) = ( 𝐷 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
3	1	fveq1i	⊢ ( 𝐷 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ‘ ⟨ 𝐴 , 𝐵 ⟩ )
4	2 3	eqtri	⊢ ( 𝐴 𝐷 𝐵 ) = ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ‘ ⟨ 𝐴 , 𝐵 ⟩ )
5		opelxpi	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ℝ × ℝ ) )
6	5	fvresd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( abs ∘ − ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
7		df-ov	⊢ ( 𝐴 ( abs ∘ − ) 𝐵 ) = ( ( abs ∘ − ) ‘ ⟨ 𝐴 , 𝐵 ⟩ )
8		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
9		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
10		eqid	⊢ ( abs ∘ − ) = ( abs ∘ − )
11	10	cnmetdval	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ( abs ∘ − ) 𝐵 ) = ( abs ‘ ( 𝐴 − 𝐵 ) ) )
12	8 9 11	syl2an	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ( abs ∘ − ) 𝐵 ) = ( abs ‘ ( 𝐴 − 𝐵 ) ) )
13	7 12	eqtr3id	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( abs ∘ − ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( abs ‘ ( 𝐴 − 𝐵 ) ) )
14	6 13	eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( abs ‘ ( 𝐴 − 𝐵 ) ) )
15	4 14	syl5eq	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 𝐷 𝐵 ) = ( abs ‘ ( 𝐴 − 𝐵 ) ) )