Theorem xmettri3

Description: Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	xmettri3	$$⊢\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\le \left(ADC\right){+}_{𝑒}\left(BDC\right)$$

Proof

Step	Hyp	Ref	Expression
1		xmettri	$$⊢\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\le \left(ADC\right){+}_{𝑒}\left(CDB\right)$$
2		xmetsym	$$⊢\left(D\in \mathrm{\infty Met}\left(X\right)\wedge B\in X\wedge C\in X\right)\to BDC=CDB$$
3	2	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=CDB$$
4	3	oveq2d	$$⊢\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(BDC\right)=\left(ADC\right){+}_{𝑒}\left(CDB\right)$$
5	1 4	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 ADB\le \left(ADC\right){+}_{𝑒}\left(BDC\right)$$