Metamath Proof Explorer

Theorem mettri

Description: Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of Gleason p. 223. (Contributed by NM, 27-Aug-2006)

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

Proof

Step Hyp Ref Expression
1 mettri2 ⊢ D ∈ Met ⁡ X ∧ C ∈ X ∧ A ∈ X ∧ B ∈ X → A D B ≤ C D A + C D B
2 1 expcom ⊢ C ∈ X ∧ A ∈ X ∧ B ∈ X → D ∈ Met ⁡ X → A D B ≤ C D A + C D B
3 2 3coml ⊢ A ∈ X ∧ B ∈ X ∧ C ∈ X → D ∈ Met ⁡ X → A D B ≤ C D A + C D B
4 3 impcom ⊢ D ∈ Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B ≤ C D A + C D B
5 metsym ⊢ D ∈ Met ⁡ X ∧ A ∈ X ∧ C ∈ X → A D C = C D A
6 5 3adant3r2 ⊢ D ∈ Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D C = C D A
7 6 oveq1d ⊢ D ∈ Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D C + C D B = C D A + C D B
8 4 7 breqtrrd ⊢ D ∈ Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B ≤ A D C + C D B