xmstri3

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	xmstri3	$⊢ (M \in ∞MetSp \land (A \in X \land B \in X \land C \in X)) \to A D B \leq (A D C) +_{𝑒} (B D C)$

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		xmettri3	$⊢ ({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) +_{𝑒} (B ({D ↾}_{(X \times X)}) C)$
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) +_{𝑒} (B ({D ↾}_{(X \times X)}) C)$
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	7 9	ovresd	$⊢ (M \in ∞MetSp \land (A \in X \land B \in X \land C \in X)) \to B ({D ↾}_{(X \times X)}) C = B D C$
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) +_{𝑒} (B ({D ↾}_{(X \times X)}) C) = (A D C) +_{𝑒} (B D C)$
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) +_{𝑒} (B D C)$

Metamath Proof Explorer