xmstri2

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

	Ref	Expression
Hypotheses	mscl.x	$⊢ X = {Base}_{M}$
	mscl.d	$⊢ D = dist (M)$
Assertion	xmstri2	$⊢ (M \in ∞MetSp \land (C \in X \land A \in X \land B \in X)) \to A D B \leq (C D A) +_{𝑒} (C 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		xmettri2	$⊢ ({D ↾}_{(X \times X)} \in ∞Met (X) \land (C \in X \land A \in X \land B \in X)) \to A ({D ↾}_{(X \times X)}) B \leq (C ({D ↾}_{(X \times X)}) A) +_{𝑒} (C ({D ↾}_{(X \times X)}) B)$
5	3 4	sylan	$⊢ (M \in ∞MetSp \land (C \in X \land A \in X \land B \in X)) \to A ({D ↾}_{(X \times X)}) B \leq (C ({D ↾}_{(X \times X)}) A) +_{𝑒} (C ({D ↾}_{(X \times X)}) B)$
6		simpr2	$⊢ (M \in ∞MetSp \land (C \in X \land A \in X \land B \in X)) \to A \in X$
7		simpr3	$⊢ (M \in ∞MetSp \land (C \in X \land A \in X \land B \in X)) \to B \in X$
8	6 7	ovresd	$⊢ (M \in ∞MetSp \land (C \in X \land A \in X \land B \in X)) \to A ({D ↾}_{(X \times X)}) B = A D B$
9		simpr1	$⊢ (M \in ∞MetSp \land (C \in X \land A \in X \land B \in X)) \to C \in X$
10	9 6	ovresd	$⊢ (M \in ∞MetSp \land (C \in X \land A \in X \land B \in X)) \to C ({D ↾}_{(X \times X)}) A = C D A$
11	9 7	ovresd	$⊢ (M \in ∞MetSp \land (C \in X \land A \in X \land B \in X)) \to C ({D ↾}_{(X \times X)}) B = C D B$
12	10 11	oveq12d	$⊢ (M \in ∞MetSp \land (C \in X \land A \in X \land B \in X)) \to (C ({D ↾}_{(X \times X)}) A) +_{𝑒} (C ({D ↾}_{(X \times X)}) B) = (C D A) +_{𝑒} (C D B)$
13	5 8 12	3brtr3d	$⊢ (M \in ∞MetSp \land (C \in X \land A \in X \land B \in X)) \to A D B \leq (C D A) +_{𝑒} (C D B)$

Metamath Proof Explorer