Theorem xrsdsval

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	xrsdsval	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to ADB=if\left(A\le B,B{+}_{𝑒}\left(-A\right),A{+}_{𝑒}\left(-B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		xrsds.d	$$⊢D=\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)$$
2		breq12	$$⊢\left(x=A\wedge y=B\right)\to \left(x\le y\leftrightarrow A\le B\right)$$
3		id	$$⊢y=B\to y=B$$
4		xnegeq	$$⊢x=A\to -x=-A$$
5	3 4	oveqan12rd	$$⊢\left(x=A\wedge y=B\right)\to y{+}_{𝑒}\left(-x\right)=B{+}_{𝑒}\left(-A\right)$$
6		id	$$⊢x=A\to x=A$$
7		xnegeq	$$⊢y=B\to -y=-B$$
8	6 7	oveqan12d	$$⊢\left(x=A\wedge y=B\right)\to x{+}_{𝑒}\left(-y\right)=A{+}_{𝑒}\left(-B\right)$$
9	2 5 8	ifbieq12d	$$⊢\left(x=A\wedge y=B\right)\to if\left(x\le y,y{+}_{𝑒}\left(-x\right),x{+}_{𝑒}\left(-y\right)\right)=if\left(A\le B,B{+}_{𝑒}\left(-A\right),A{+}_{𝑒}\left(-B\right)\right)$$
10	1	xrsds	$$⊢D=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼if\left(x\le y,y{+}_{𝑒}\left(-x\right),x{+}_{𝑒}\left(-y\right)\right)\right)$$
11		ovex	$$⊢B{+}_{𝑒}\left(-A\right)\in \mathrm{V}$$
12		ovex	$$⊢A{+}_{𝑒}\left(-B\right)\in \mathrm{V}$$
13	11 12	ifex	$$⊢if\left(A\le B,B{+}_{𝑒}\left(-A\right),A{+}_{𝑒}\left(-B\right)\right)\in \mathrm{V}$$
14	9 10 13	ovmpoa	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to ADB=if\left(A\le B,B{+}_{𝑒}\left(-A\right),A{+}_{𝑒}\left(-B\right)\right)$$