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