Metamath Proof Explorer

Theorem cnmetdval

Description: Value of the distance function of the metric space of complex numbers. (Contributed by NM, 9-Dec-2006) (Revised by Mario Carneiro, 27-Dec-2014)

Ref Expression
Hypothesis cnmetdval.1 ${⊢}{D}=\mathrm{abs}\circ -$
Assertion cnmetdval ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}{D}{B}=\left|{A}-{B}\right|$

Proof

Step Hyp Ref Expression
1 cnmetdval.1 ${⊢}{D}=\mathrm{abs}\circ -$
2 subf ${⊢}-:ℂ×ℂ⟶ℂ$
3 opelxpi ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to ⟨{A},{B}⟩\in \left(ℂ×ℂ\right)$
4 fvco3 ${⊢}\left(-:ℂ×ℂ⟶ℂ\wedge ⟨{A},{B}⟩\in \left(ℂ×ℂ\right)\right)\to \left(\mathrm{abs}\circ -\right)\left(⟨{A},{B}⟩\right)=\left|-\left(⟨{A},{B}⟩\right)\right|$
5 2 3 4 sylancr ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left(\mathrm{abs}\circ -\right)\left(⟨{A},{B}⟩\right)=\left|-\left(⟨{A},{B}⟩\right)\right|$
6 df-ov ${⊢}{A}{D}{B}={D}\left(⟨{A},{B}⟩\right)$
7 1 fveq1i ${⊢}{D}\left(⟨{A},{B}⟩\right)=\left(\mathrm{abs}\circ -\right)\left(⟨{A},{B}⟩\right)$
8 6 7 eqtri ${⊢}{A}{D}{B}=\left(\mathrm{abs}\circ -\right)\left(⟨{A},{B}⟩\right)$
9 df-ov ${⊢}{A}-{B}=-\left(⟨{A},{B}⟩\right)$
10 9 fveq2i ${⊢}\left|{A}-{B}\right|=\left|-\left(⟨{A},{B}⟩\right)\right|$
11 5 8 10 3eqtr4g ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}{D}{B}=\left|{A}-{B}\right|$