Metamath Proof Explorer

Theorem metrtri

Description: Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 5-May-2014)

Ref Expression
Assertion metrtri ⊢ D ∈ Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D C − B D C ≤ A D B

Proof

Step Hyp Ref Expression
1 metcl ⊢ D ∈ Met ⁡ X ∧ A ∈ X ∧ C ∈ X → A D C ∈ ℝ
2 1 3adant3r2 ⊢ D ∈ Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D C ∈ ℝ
3 metcl ⊢ D ∈ Met ⁡ X ∧ B ∈ X ∧ C ∈ X → B D C ∈ ℝ
4 3 3adant3r1 ⊢ D ∈ Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B D C ∈ ℝ
5 eqid ⊢ dist ⁡ ℝ 𝑠 * = dist ⁡ ℝ 𝑠 *
6 5 xrsdsreval ⊢ A D C ∈ ℝ ∧ B D C ∈ ℝ → A D C dist ⁡ ℝ 𝑠 * B D C = A D C − B D C
7 2 4 6 syl2anc ⊢ D ∈ Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D C dist ⁡ ℝ 𝑠 * B D C = A D C − B D C
8 metxmet ⊢ D ∈ Met ⁡ X → D ∈ ∞Met ⁡ X
9 5 xmetrtri2 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D C dist ⁡ ℝ 𝑠 * B D C ≤ A D B
10 8 9 sylan ⊢ D ∈ Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D C dist ⁡ ℝ 𝑠 * B D C ≤ A D B
11 7 10 eqbrtrrd ⊢ D ∈ Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D C − B D C ≤ A D B