This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 𝐷 𝐵 ) = ( abs ‘ ( 𝐴 − 𝐵 ) ) )