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 = {Base}_{M}$
	mscl.d	$⊢ D = dist (M)$
Assertion	xmsge0	$⊢ (M \in ∞MetSp \land A \in X \land B \in X) \to 0 \leq A D B$

Step	Hyp	Ref	Expression
1		mscl.x	$⊢ X = {Base}_{M}$
2		mscl.d	$⊢ D = dist (M)$
3	1 2	xmsxmet2	$⊢ M \in ∞MetSp \to {D ↾}_{(X \times X)} \in ∞Met (X)$
4		xmetge0	$⊢ ({D ↾}_{(X \times X)} \in ∞Met (X) \land A \in X \land B \in X) \to 0 \leq A ({D ↾}_{(X \times X)}) B$
5	3 4	syl3an1	$⊢ (M \in ∞MetSp \land A \in X \land B \in X) \to 0 \leq A ({D ↾}_{(X \times X)}) B$
6		ovres	$⊢ (A \in X \land B \in X) \to A ({D ↾}_{(X \times X)}) B = A D B$
7	6	3adant1	$⊢ (M \in ∞MetSp \land A \in X \land B \in X) \to A ({D ↾}_{(X \times X)}) B = A D B$
8	5 7	breqtrd	$⊢ (M \in ∞MetSp \land A \in X \land B \in X) \to 0 \leq A D B$

Metamath Proof Explorer