Metamath Proof Explorer

Theorem msrtri

Description: Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses mscl.x ⊢ X = Base M
mscl.d ⊢ D = dist ⁡ M
Assertion msrtri ⊢ M ∈ MetSp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D C − B D C ≤ A D B

Proof

Step Hyp Ref Expression
1 mscl.x ⊢ X = Base M
2 mscl.d ⊢ D = dist ⁡ M
3 1 2 msmet2 ⊢ M ∈ MetSp → D ↾ X × X ∈ Met ⁡ X
4 metrtri ⊢ D ↾ X × X ∈ Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D ↾ X × X C − B D ↾ X × X C ≤ A D ↾ X × X B
5 3 4 sylan ⊢ M ∈ MetSp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D ↾ X × X C − B D ↾ X × X C ≤ A D ↾ X × X B
6 simpr1 ⊢ M ∈ MetSp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A ∈ X
7 simpr3 ⊢ M ∈ MetSp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → C ∈ X
8 6 7 ovresd ⊢ M ∈ MetSp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D ↾ X × X C = A D C
9 simpr2 ⊢ M ∈ MetSp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B ∈ X
10 9 7 ovresd ⊢ M ∈ MetSp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B D ↾ X × X C = B D C
11 8 10 oveq12d ⊢ M ∈ MetSp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D ↾ X × X C − B D ↾ X × X C = A D C − B D C
12 11 fveq2d ⊢ M ∈ MetSp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D ↾ X × X C − B D ↾ X × X C = A D C − B D C
13 6 9 ovresd ⊢ M ∈ MetSp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D ↾ X × X B = A D B
14 5 12 13 3brtr3d ⊢ M ∈ MetSp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D C − B D C ≤ A D B