Metamath Proof Explorer

Theorem mettri3

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

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

Proof

Step Hyp Ref Expression
1 mettri ⊢ D ∈ Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B ≤ A D C + C D B
2 metsym ⊢ D ∈ Met ⁡ X ∧ B ∈ X ∧ C ∈ X → B D C = C D B
3 2 3adant3r1 ⊢ D ∈ Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B D C = C D B
4 3 oveq2d ⊢ D ∈ Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D C + B D C = A D C + C D B
5 1 4 breqtrrd ⊢ D ∈ Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B ≤ A D C + B D C