Metamath Proof Explorer

Theorem xmettri

Description: Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of Gleason p. 223. (Contributed by Mario Carneiro, 20-Aug-2015)

		Ref	Expression
	Assertion	xmettri	$⊢ (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		simpl	$⊢ (D \in ∞Met (X) \land (A \in X \land B \in X \land C \in X)) \to D \in ∞Met (X)$
2		simpr3	$⊢ (D \in ∞Met (X) \land (A \in X \land B \in X \land C \in X)) \to C \in X$
3		simpr1	$⊢ (D \in ∞Met (X) \land (A \in X \land B \in X \land C \in X)) \to A \in X$
4		simpr2	$⊢ (D \in ∞Met (X) \land (A \in X \land B \in X \land C \in X)) \to B \in X$
5		xmettri2	$⊢ (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)$
6	1 2 3 4 5	syl13anc	$⊢ (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)$
7		xmetsym	$⊢ (D \in ∞Met (X) \land C \in X \land A \in X) \to C D A = A D C$
8	1 2 3 7	syl3anc	$⊢ (D \in ∞Met (X) \land (A \in X \land B \in X \land C \in X)) \to C D A = A D C$
9	8	oveq1d	$⊢ (D \in ∞Met (X) \land (A \in X \land B \in X \land C \in X)) \to (C D A) +_{𝑒} (C D B) = (A D C) +_{𝑒} (C D B)$
10	6 9	breqtrd	$⊢ (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)$