mstri3

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

	Ref	Expression
Hypotheses	mscl.x	$⊢ X = {Base}_{M}$
	mscl.d	$⊢ D = dist (M)$
Assertion	mstri3	$⊢ (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	msmet2	$⊢ M \in MetSp \to {D ↾}_{(X \times X)} \in Met (X)$
4		mettri3	$⊢ ({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