Metamath Proof Explorer

Theorem mettri

Description: Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of Gleason p. 223. (Contributed by NM, 27-Aug-2006)

		Ref	Expression
	Assertion	mettri	$⊢ (D \in Met (X) \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		mettri2	$⊢ (D \in Met (X) \land (C \in X \land A \in X \land B \in X)) \to A D B \leq (C D A) + (C D B)$
2	1	expcom	$⊢ (C \in X \land A \in X \land B \in X) \to (D \in Met (X) \to A D B \leq (C D A) + (C D B))$
3	2	3coml	$⊢ (A \in X \land B \in X \land C \in X) \to (D \in Met (X) \to A D B \leq (C D A) + (C D B))$
4	3	impcom	$⊢ (D \in Met (X) \land (A \in X \land B \in X \land C \in X)) \to A D B \leq (C D A) + (C D B)$
5		metsym	$⊢ (D \in Met (X) \land A \in X \land C \in X) \to A D C = C D A$
6	5	3adant3r2	$⊢ (D \in Met (X) \land (A \in X \land B \in X \land C \in X)) \to A D C = C D A$
7	6	oveq1d	$⊢ (D \in Met (X) \land (A \in X \land B \in X \land C \in X)) \to (A D C) + (C D B) = (C D A) + (C D B)$
8	4 7	breqtrrd	$⊢ (D \in Met (X) \land (A \in X \land B \in X \land C \in X)) \to A D B \leq (A D C) + (C D B)$