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 ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B ≤ A D C + 𝑒 C D B

Proof

Step Hyp Ref Expression
1 simpl ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → D ∈ ∞Met ⁡ X
2 simpr3 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → C ∈ X
3 simpr1 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A ∈ X
4 simpr2 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B ∈ X
5 xmettri2 ⊢ D ∈ ∞Met ⁡ X ∧ C ∈ X ∧ A ∈ X ∧ B ∈ X → A D B ≤ C D A + 𝑒 C D B
6 1 2 3 4 5 syl13anc ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B ≤ C D A + 𝑒 C D B
7 xmetsym ⊢ D ∈ ∞Met ⁡ X ∧ C ∈ X ∧ A ∈ X → C D A = A D C
8 1 2 3 7 syl3anc ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → C D A = A D C
9 8 oveq1d ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → C D A + 𝑒 C D B = A D C + 𝑒 C D B
10 6 9 breqtrd ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B ≤ A D C + 𝑒 C D B