mettri3

Description: Triangle inequality for the distance function of a metric space. (Contributed by NM, 13-Mar-2007)

		Ref	Expression
	Assertion	mettri3	$⊢ (D \in Met (X) \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		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)$
2		metsym	$⊢ (D \in Met (X) \land B \in X \land C \in X) \to B D C = C D B$
3	2	3adant3r1	$⊢ (D \in Met (X) \land (A \in X \land B \in X \land C \in X)) \to B D C = C D B$
4	3	oveq2d	$⊢ (D \in Met (X) \land (A \in X \land B \in X \land C \in X)) \to (A D C) + (B D C) = (A D C) + (C D B)$
5	1 4	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) + (B D C)$

Metamath Proof Explorer