This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xmettri3

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

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

Proof

Step Hyp Ref Expression
1 xmettri ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B ≤ A D C + 𝑒 C D B
2 xmetsym ⊢ 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