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	$$⊢D={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}$$
Assertion	remetdval	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to ADB=\left|A-B\right|$$

Proof

Step	Hyp	Ref	Expression
1		remet.1	$$⊢D={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}$$
2		df-ov	$$⊢ADB=D\left(⟨A,B⟩\right)$$
3	1	fveq1i	$$⊢D\left(⟨A,B⟩\right)=\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)\left(⟨A,B⟩\right)$$
4	2 3	eqtri	$$⊢ADB=\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)\left(⟨A,B⟩\right)$$
5		opelxpi	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to ⟨A,B⟩\in {ℝ}^2$$
6	5	fvresd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)\left(⟨A,B⟩\right)=\left(\mathrm{abs}\circ -\right)\left(⟨A,B⟩\right)$$
7		df-ov	$$⊢A\left(\mathrm{abs}\circ -\right)B=\left(\mathrm{abs}\circ -\right)\left(⟨A,B⟩\right)$$
8		recn	$$⊢A\in ℝ\to A\in ℂ$$
9		recn	$$⊢B\in ℝ\to B\in ℂ$$
10		eqid	$$⊢\mathrm{abs}\circ -=\mathrm{abs}\circ -$$
11	10	cnmetdval	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A\left(\mathrm{abs}\circ -\right)B=\left|A-B\right|$$
12	8 9 11	syl2an	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A\left(\mathrm{abs}\circ -\right)B=\left|A-B\right|$$
13	7 12	eqtr3id	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(\mathrm{abs}\circ -\right)\left(⟨A,B⟩\right)=\left|A-B\right|$$
14	6 13	eqtrd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)\left(⟨A,B⟩\right)=\left|A-B\right|$$
15	4 14	eqtrid	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to ADB=\left|A-B\right|$$