Theorem xmetrtri2

Description: The reverse triangle inequality for the distance function of an extended metric. In order to express the "extended absolute value function", we use the distance function xrsdsval defined on the extended real structure. (Contributed by Mario Carneiro, 4-Sep-2015)

	Ref	Expression
Hypothesis	xmetrtri2.1	$$⊢K=\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)$$
Assertion	xmetrtri2	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge \left(A\in X\wedge B\in X\wedge C\in X\right)\right)\to \left(ADC\right)K\left(BDC\right)\le ADB$$

Proof

Step	Hyp	Ref	Expression
1		xmetrtri2.1	$$⊢K=\mathrm{dist}\left({ℝ}_{𝑠}^{*}\right)$$
2		xmetcl	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge A\in X\wedge C\in X\right)\to ADC\in {ℝ}^{*}$$
3	2	3adant3r2	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge \left(A\in X\wedge B\in X\wedge C\in X\right)\right)\to ADC\in {ℝ}^{*}$$
4		xmetcl	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge B\in X\wedge C\in X\right)\to BDC\in {ℝ}^{*}$$
5	4	3adant3r1	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge \left(A\in X\wedge B\in X\wedge C\in X\right)\right)\to BDC\in {ℝ}^{*}$$
6	1	xrsdsval	$$⊢\left(ADC\in {ℝ}^{*}\wedge BDC\in {ℝ}^{*}\right)\to \left(ADC\right)K\left(BDC\right)=if\left(ADC\le BDC,\left(BDC\right){+}_{𝑒}\left(-\left(ADC\right)\right),\left(ADC\right){+}_{𝑒}\left(-\left(BDC\right)\right)\right)$$
7	3 5 6	syl2anc	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge \left(A\in X\wedge B\in X\wedge C\in X\right)\right)\to \left(ADC\right)K\left(BDC\right)=if\left(ADC\le BDC,\left(BDC\right){+}_{𝑒}\left(-\left(ADC\right)\right),\left(ADC\right){+}_{𝑒}\left(-\left(BDC\right)\right)\right)$$
8		3ancoma	$$⊢\left(A\in X\wedge B\in X\wedge C\in X\right)\leftrightarrow \left(B\in X\wedge A\in X\wedge C\in X\right)$$
9		xmetrtri	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge \left(B\in X\wedge A\in X\wedge C\in X\right)\right)\to \left(BDC\right){+}_{𝑒}\left(-\left(ADC\right)\right)\le BDA$$
10	8 9	sylan2b	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge \left(A\in X\wedge B\in X\wedge C\in X\right)\right)\to \left(BDC\right){+}_{𝑒}\left(-\left(ADC\right)\right)\le BDA$$
11		xmetsym	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge A\in X\wedge B\in X\right)\to ADB=BDA$$
12	11	3adant3r3	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge \left(A\in X\wedge B\in X\wedge C\in X\right)\right)\to ADB=BDA$$
13	10 12	breqtrrd	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge \left(A\in X\wedge B\in X\wedge C\in X\right)\right)\to \left(BDC\right){+}_{𝑒}\left(-\left(ADC\right)\right)\le ADB$$
14		xmetrtri	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge \left(A\in X\wedge B\in X\wedge C\in X\right)\right)\to \left(ADC\right){+}_{𝑒}\left(-\left(BDC\right)\right)\le ADB$$
15		breq1	$$⊢\left(BDC\right){+}_{𝑒}\left(-\left(ADC\right)\right)=if\left(ADC\le BDC,\left(BDC\right){+}_{𝑒}\left(-\left(ADC\right)\right),\left(ADC\right){+}_{𝑒}\left(-\left(BDC\right)\right)\right)\to \left(\left(BDC\right){+}_{𝑒}\left(-\left(ADC\right)\right)\le ADB\leftrightarrow if\left(ADC\le BDC,\left(BDC\right){+}_{𝑒}\left(-\left(ADC\right)\right),\left(ADC\right){+}_{𝑒}\left(-\left(BDC\right)\right)\right)\le ADB\right)$$
16		breq1	$$⊢\left(ADC\right){+}_{𝑒}\left(-\left(BDC\right)\right)=if\left(ADC\le BDC,\left(BDC\right){+}_{𝑒}\left(-\left(ADC\right)\right),\left(ADC\right){+}_{𝑒}\left(-\left(BDC\right)\right)\right)\to \left(\left(ADC\right){+}_{𝑒}\left(-\left(BDC\right)\right)\le ADB\leftrightarrow if\left(ADC\le BDC,\left(BDC\right){+}_{𝑒}\left(-\left(ADC\right)\right),\left(ADC\right){+}_{𝑒}\left(-\left(BDC\right)\right)\right)\le ADB\right)$$
17	15 16	ifboth	$$⊢\left(\left(BDC\right){+}_{𝑒}\left(-\left(ADC\right)\right)\le ADB\wedge \left(ADC\right){+}_{𝑒}\left(-\left(BDC\right)\right)\le ADB\right)\to if\left(ADC\le BDC,\left(BDC\right){+}_{𝑒}\left(-\left(ADC\right)\right),\left(ADC\right){+}_{𝑒}\left(-\left(BDC\right)\right)\right)\le ADB$$
18	13 14 17	syl2anc	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge \left(A\in X\wedge B\in X\wedge C\in X\right)\right)\to if\left(ADC\le BDC,\left(BDC\right){+}_{𝑒}\left(-\left(ADC\right)\right),\left(ADC\right){+}_{𝑒}\left(-\left(BDC\right)\right)\right)\le ADB$$
19	7 18	eqbrtrd	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge \left(A\in X\wedge B\in X\wedge C\in X\right)\right)\to \left(ADC\right)K\left(BDC\right)\le ADB$$