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