Theorem xrsdsre

Description: The metric on the extended reals coincides with the usual metric on the reals. (Contributed by Mario Carneiro, 4-Sep-2015)

	Ref	Expression
Hypothesis	xrsxmet.1	$$⊢D=\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)$$
Assertion	xrsdsre	$$⊢{D\upharpoonright }_{{ℝ}^2}={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}$$

Proof

Step	Hyp	Ref	Expression
1		xrsxmet.1	$$⊢D=\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)$$
2	1	xrsdsreval	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to xDy=\left|x-y\right|$$
3		ovres	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x\left({D\upharpoonright }_{{ℝ}^2}\right)y=xDy$$
4		eqid	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}$$
5	4	remetdval	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)y=\left|x-y\right|$$
6	2 3 5	3eqtr4d	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x\left({D\upharpoonright }_{{ℝ}^2}\right)y=x\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)y$$
7	6	rgen2	$$⊢\forall x\in ℝ\forall y\in ℝx\left({D\upharpoonright }_{{ℝ}^2}\right)y=x\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)y$$
8	1	xrsxmet	$$⊢D\in \mathrm{\infty Met}\left({ℝ}^{*}\right)$$
9		xmetf	$$⊢D\in \mathrm{\infty Met}\left({ℝ}^{*}\right)\to D:{ℝ}^{*}\times {ℝ}^{*}⟶{ℝ}^{*}$$
10		ffn	$$⊢D:{ℝ}^{*}\times {ℝ}^{*}⟶{ℝ}^{*}\to DFn\left({ℝ}^{*}\times {ℝ}^{*}\right)$$
11	8 9 10	mp2b	$$⊢DFn\left({ℝ}^{*}\times {ℝ}^{*}\right)$$
12		rexpssxrxp	$$⊢{ℝ}^2\subseteq {ℝ}^{*}\times {ℝ}^{*}$$
13		fnssres	$$⊢\left(DFn\left({ℝ}^{*}\times {ℝ}^{*}\right)\wedge {ℝ}^2\subseteq {ℝ}^{*}\times {ℝ}^{*}\right)\to \left({D\upharpoonright }_{{ℝ}^2}\right)Fn{ℝ}^2$$
14	11 12 13	mp2an	$$⊢\left({D\upharpoonright }_{{ℝ}^2}\right)Fn{ℝ}^2$$
15		cnmet	$$⊢\mathrm{abs}\circ -\in \mathrm{Met}\left(ℂ\right)$$
16		metf	$$⊢\mathrm{abs}\circ -\in \mathrm{Met}\left(ℂ\right)\to \left(\mathrm{abs}\circ -\right):ℂ\times ℂ⟶ℝ$$
17		ffn	$$⊢\left(\mathrm{abs}\circ -\right):ℂ\times ℂ⟶ℝ\to \left(\mathrm{abs}\circ -\right)Fn\left(ℂ\times ℂ\right)$$
18	15 16 17	mp2b	$$⊢\left(\mathrm{abs}\circ -\right)Fn\left(ℂ\times ℂ\right)$$
19		ax-resscn	$$⊢ℝ\subseteq ℂ$$
20		xpss12	$$⊢\left(ℝ\subseteq ℂ\wedge ℝ\subseteq ℂ\right)\to {ℝ}^2\subseteq ℂ\times ℂ$$
21	19 19 20	mp2an	$$⊢{ℝ}^2\subseteq ℂ\times ℂ$$
22		fnssres	$$⊢\left(\left(\mathrm{abs}\circ -\right)Fn\left(ℂ\times ℂ\right)\wedge {ℝ}^2\subseteq ℂ\times ℂ\right)\to \left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)Fn{ℝ}^2$$
23	18 21 22	mp2an	$$⊢\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)Fn{ℝ}^2$$
24		eqfnov2	$$⊢\left(\left({D\upharpoonright }_{{ℝ}^2}\right)Fn{ℝ}^2\wedge \left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)Fn{ℝ}^2\right)\to \left({D\upharpoonright }_{{ℝ}^2}={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\leftrightarrow \forall x\in ℝ\forall y\in ℝx\left({D\upharpoonright }_{{ℝ}^2}\right)y=x\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)y\right)$$
25	14 23 24	mp2an	$$⊢{D\upharpoonright }_{{ℝ}^2}={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\leftrightarrow \forall x\in ℝ\forall y\in ℝx\left({D\upharpoonright }_{{ℝ}^2}\right)y=x\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)y$$
26	7 25	mpbir	$$⊢{D\upharpoonright }_{{ℝ}^2}={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}$$