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 ADB=\left|A-B\right|$$

Proof

Step	Hyp	Ref	Expression
1		cnmetdval.1	$$⊢D=\mathrm{abs}\circ -$$
2		subf	$$⊢-:ℂ\times ℂ⟶ℂ$$
3		opelxpi	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to ⟨A,B⟩\in \left(ℂ\times ℂ\right)$$
4		fvco3	$$⊢\left(-:ℂ\times ℂ⟶ℂ\wedge ⟨A,B⟩\in \left(ℂ\times ℂ\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	$$⊢ADB=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	$$⊢ADB=\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 ADB=\left|A-B\right|$$