Metamath Proof Explorer

Theorem xmstri3

Description: Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 2-Oct-2015)

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

Proof

Step Hyp Ref Expression
1 mscl.x ⊢ X = Base M
2 mscl.d ⊢ D = dist ⁡ M
3 1 2 xmsxmet2 ⊢ M ∈ ∞MetSp → D ↾ X × X ∈ ∞Met ⁡ X
4 xmettri3 ⊢ D ↾ X × X ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D ↾ X × X B ≤ A D ↾ X × X C + 𝑒 B D ↾ X × X C
5 3 4 sylan ⊢ M ∈ ∞MetSp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D ↾ X × X B ≤ A D ↾ X × X C + 𝑒 B D ↾ X × X C
6 simpr1 ⊢ M ∈ ∞MetSp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A ∈ X
7 simpr2 ⊢ M ∈ ∞MetSp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B ∈ X
8 6 7 ovresd ⊢ M ∈ ∞MetSp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D ↾ X × X B = A D B
9 simpr3 ⊢ M ∈ ∞MetSp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → C ∈ X
10 6 9 ovresd ⊢ M ∈ ∞MetSp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D ↾ X × X C = A D C
11 7 9 ovresd ⊢ M ∈ ∞MetSp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B D ↾ X × X C = B D C
12 10 11 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
13 5 8 12 3brtr3d ⊢ M ∈ ∞MetSp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B ≤ A D C + 𝑒 B D C