Theorem xmsge0

Description: The distance function in an extended metric space is nonnegative. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	mscl.x	$$⊢X={\mathrm{Base}}_M$$
	mscl.d	$$⊢D=\mathrm{dist}\left(M\right)$$
Assertion	xmsge0	$$⊢\left(M\in \mathrm{\infty MetSp}\wedge A\in X\wedge B\in X\right)\to 0\le ADB$$

Proof

Step	Hyp	Ref	Expression
1		mscl.x	$$⊢X={\mathrm{Base}}_M$$
2		mscl.d	$$⊢D=\mathrm{dist}\left(M\right)$$
3	1 2	xmsxmet2	$$⊢M\in \mathrm{\infty MetSp}\to {D\upharpoonright }_{\left(X\times X\right)}\in \mathrm{\infty Met}\left(X\right)$$
4		xmetge0	$$⊢\left({D\upharpoonright }_{\left(X\times X\right)}\in \mathrm{\infty Met}\left(X\right)\wedge A\in X\wedge B\in X\right)\to 0\le A\left({D\upharpoonright }_{\left(X\times X\right)}\right)B$$
5	3 4	syl3an1	$$⊢\left(M\in \mathrm{\infty MetSp}\wedge A\in X\wedge B\in X\right)\to 0\le A\left({D\upharpoonright }_{\left(X\times X\right)}\right)B$$
6		ovres	$$⊢\left(A\in X\wedge B\in X\right)\to A\left({D\upharpoonright }_{\left(X\times X\right)}\right)B=ADB$$
7	6	3adant1	$$⊢\left(M\in \mathrm{\infty MetSp}\wedge A\in X\wedge B\in X\right)\to A\left({D\upharpoonright }_{\left(X\times X\right)}\right)B=ADB$$
8	5 7	breqtrd	$$⊢\left(M\in \mathrm{\infty MetSp}\wedge A\in X\wedge B\in X\right)\to 0\le ADB$$