Metamath Proof Explorer

Theorem mettri2

Description: Triangle inequality for the distance function of a metric space. (Contributed by NM, 30-Aug-2006) (Revised by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion mettri2 ⊢ D ∈ Met ⁡ X ∧ C ∈ X ∧ A ∈ X ∧ B ∈ X → A D B ≤ C D A + C D B

Proof

Step Hyp Ref Expression
1 metxmet ⊢ D ∈ Met ⁡ X → D ∈ ∞Met ⁡ X
2 xmettri2 ⊢ D ∈ ∞Met ⁡ X ∧ C ∈ X ∧ A ∈ X ∧ B ∈ X → A D B ≤ C D A + 𝑒 C D B
3 1 2 sylan ⊢ D ∈ Met ⁡ X ∧ C ∈ X ∧ A ∈ X ∧ B ∈ X → A D B ≤ C D A + 𝑒 C D B
4 metcl ⊢ D ∈ Met ⁡ X ∧ C ∈ X ∧ A ∈ X → C D A ∈ ℝ
5 4 3adant3r3 ⊢ D ∈ Met ⁡ X ∧ C ∈ X ∧ A ∈ X ∧ B ∈ X → C D A ∈ ℝ
6 metcl ⊢ D ∈ Met ⁡ X ∧ C ∈ X ∧ B ∈ X → C D B ∈ ℝ
7 6 3adant3r2 ⊢ D ∈ Met ⁡ X ∧ C ∈ X ∧ A ∈ X ∧ B ∈ X → C D B ∈ ℝ
8 5 7 rexaddd ⊢ D ∈ Met ⁡ X ∧ C ∈ X ∧ A ∈ X ∧ B ∈ X → C D A + 𝑒 C D B = C D A + C D B
9 3 8 breqtrd ⊢ D ∈ Met ⁡ X ∧ C ∈ X ∧ A ∈ X ∧ B ∈ X → A D B ≤ C D A + C D B