Theorem xrsds

Description: The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Hypothesis	xrsds.d	$$⊢D=\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)$$
Assertion	xrsds	$$⊢D=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼if\left(x\le y,y{+}_{𝑒}\left(-x\right),x{+}_{𝑒}\left(-y\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		xrsds.d	$$⊢D=\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)$$
2		id	$$⊢y\in {ℝ}^{*}\to y\in {ℝ}^{*}$$
3		xnegcl	$$⊢x\in {ℝ}^{*}\to -x\in {ℝ}^{*}$$
4		xaddcl	$$⊢\left(y\in {ℝ}^{*}\wedge -x\in {ℝ}^{*}\right)\to y{+}_{𝑒}\left(-x\right)\in {ℝ}^{*}$$
5	2 3 4	syl2anr	$$⊢\left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to y{+}_{𝑒}\left(-x\right)\in {ℝ}^{*}$$
6		xnegcl	$$⊢y\in {ℝ}^{*}\to -y\in {ℝ}^{*}$$
7		xaddcl	$$⊢\left(x\in {ℝ}^{*}\wedge -y\in {ℝ}^{*}\right)\to x{+}_{𝑒}\left(-y\right)\in {ℝ}^{*}$$
8	6 7	sylan2	$$⊢\left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to x{+}_{𝑒}\left(-y\right)\in {ℝ}^{*}$$
9	5 8	ifcld	$$⊢\left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to if\left(x\le y,y{+}_{𝑒}\left(-x\right),x{+}_{𝑒}\left(-y\right)\right)\in {ℝ}^{*}$$
10	9	rgen2	$$⊢\forall x\in {ℝ}^{*}\forall y\in {ℝ}^{*}if\left(x\le y,y{+}_{𝑒}\left(-x\right),x{+}_{𝑒}\left(-y\right)\right)\in {ℝ}^{*}$$
11		eqid	$$⊢\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼if\left(x\le y,y{+}_{𝑒}\left(-x\right),x{+}_{𝑒}\left(-y\right)\right)\right)=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼if\left(x\le y,y{+}_{𝑒}\left(-x\right),x{+}_{𝑒}\left(-y\right)\right)\right)$$
12	11	fmpo	$$⊢\forall x\in {ℝ}^{*}\forall y\in {ℝ}^{*}if\left(x\le y,y{+}_{𝑒}\left(-x\right),x{+}_{𝑒}\left(-y\right)\right)\in {ℝ}^{*}\leftrightarrow \left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼if\left(x\le y,y{+}_{𝑒}\left(-x\right),x{+}_{𝑒}\left(-y\right)\right)\right):{ℝ}^{*}\times {ℝ}^{*}⟶{ℝ}^{*}$$
13	10 12	mpbi	$$⊢\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼if\left(x\le y,y{+}_{𝑒}\left(-x\right),x{+}_{𝑒}\left(-y\right)\right)\right):{ℝ}^{*}\times {ℝ}^{*}⟶{ℝ}^{*}$$
14		xrex	$$⊢{ℝ}^{*}\in \mathrm{V}$$
15	14 14	xpex	$$⊢{ℝ}^{*}\times {ℝ}^{*}\in \mathrm{V}$$
16		fex2	$$⊢\left(\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼if\left(x\le y,y{+}_{𝑒}\left(-x\right),x{+}_{𝑒}\left(-y\right)\right)\right):{ℝ}^{*}\times {ℝ}^{*}⟶{ℝ}^{*}\wedge {ℝ}^{*}\times {ℝ}^{*}\in \mathrm{V}\wedge {ℝ}^{*}\in \mathrm{V}\right)\to \left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼if\left(x\le y,y{+}_{𝑒}\left(-x\right),x{+}_{𝑒}\left(-y\right)\right)\right)\in \mathrm{V}$$
17	13 15 14 16	mp3an	$$⊢\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼if\left(x\le y,y{+}_{𝑒}\left(-x\right),x{+}_{𝑒}\left(-y\right)\right)\right)\in \mathrm{V}$$
18		df-xrs	$$⊢{ℝ}_{𝑠}^{*}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{ℝ}^{*}⟩,⟨{+}_{\mathrm{ndx}},{+}_{𝑒}⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_{𝑒}⟩\right\}\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{ordTop}\left(\le \right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼if\left(x\le y,y{+}_{𝑒}\left(-x\right),x{+}_{𝑒}\left(-y\right)\right)\right)⟩\right\}$$
19	18	odrngds	$$⊢\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼if\left(x\le y,y{+}_{𝑒}\left(-x\right),x{+}_{𝑒}\left(-y\right)\right)\right)\in \mathrm{V}\to \left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼if\left(x\le y,y{+}_{𝑒}\left(-x\right),x{+}_{𝑒}\left(-y\right)\right)\right)=\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)$$
20	17 19	ax-mp	$$⊢\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼if\left(x\le y,y{+}_{𝑒}\left(-x\right),x{+}_{𝑒}\left(-y\right)\right)\right)=\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)$$
21	1 20	eqtr4i	$$⊢D=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼if\left(x\le y,y{+}_{𝑒}\left(-x\right),x{+}_{𝑒}\left(-y\right)\right)\right)$$