Metamath Proof Explorer

Theorem xmstri

Description: Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of Gleason p. 223. (Contributed by Mario Carneiro, 2-Oct-2015)

		Ref	Expression
	Hypotheses	mscl.x	$⊢ X = {Base}_{M}$
		mscl.d	$⊢ D = dist (M)$
	Assertion	xmstri	$⊢ (M \in ∞MetSp \land (A \in X \land B \in X \land C \in X)) \to A D B \leq (A D C) +_{𝑒} (C D B)$

Proof

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		xmettri	$⊢ ({D ↾}_{(X \times X)} \in ∞Met (X) \land (A \in X \land B \in X \land C \in X)) \to A ({D ↾}_{(X \times X)}) B \leq (A ({D ↾}_{(X \times X)}) C) +_{𝑒} (C ({D ↾}_{(X \times X)}) B)$
5	3 4	sylan	$⊢ (M \in ∞MetSp \land (A \in X \land B \in X \land C \in X)) \to A ({D ↾}_{(X \times X)}) B \leq (A ({D ↾}_{(X \times X)}) C) +_{𝑒} (C ({D ↾}_{(X \times X)}) B)$
6		simpr1	$⊢ (M \in ∞MetSp \land (A \in X \land B \in X \land C \in X)) \to A \in X$
7		simpr2	$⊢ (M \in ∞MetSp \land (A \in X \land B \in X \land C \in X)) \to B \in X$
8	6 7	ovresd	$⊢ (M \in ∞MetSp \land (A \in X \land B \in X \land C \in X)) \to A ({D ↾}_{(X \times X)}) B = A D B$
9		simpr3	$⊢ (M \in ∞MetSp \land (A \in X \land B \in X \land C \in X)) \to C \in X$
10	6 9	ovresd	$⊢ (M \in ∞MetSp \land (A \in X \land B \in X \land C \in X)) \to A ({D ↾}_{(X \times X)}) C = A D C$
11	9 7	ovresd	$⊢ (M \in ∞MetSp \land (A \in X \land B \in X \land C \in X)) \to C ({D ↾}_{(X \times X)}) B = C D B$
12	10 11	oveq12d	$⊢ (M \in ∞MetSp \land (A \in X \land B \in X \land C \in X)) \to (A ({D ↾}_{(X \times X)}) C) +_{𝑒} (C ({D ↾}_{(X \times X)}) B) = (A D C) +_{𝑒} (C D B)$
13	5 8 12	3brtr3d	$⊢ (M \in ∞MetSp \land (A \in X \land B \in X \land C \in X)) \to A D B \leq (A D C) +_{𝑒} (C D B)$