Metamath Proof Explorer


Theorem xmstri2

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 xmstri2 M ∞MetSp C X A X B X A D B C D A + 𝑒 C D B

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 xmettri2 D X × X ∞Met X C X A X B X A D X × X B C D X × X A + 𝑒 C D X × X B
5 3 4 sylan M ∞MetSp C X A X B X A D X × X B C D X × X A + 𝑒 C D X × X B
6 simpr2 M ∞MetSp C X A X B X A X
7 simpr3 M ∞MetSp C X A X B X B X
8 6 7 ovresd M ∞MetSp C X A X B X A D X × X B = A D B
9 simpr1 M ∞MetSp C X A X B X C X
10 9 6 ovresd M ∞MetSp C X A X B X C D X × X A = C D A
11 9 7 ovresd M ∞MetSp C X A X B X C D X × X B = C D B
12 10 11 oveq12d M ∞MetSp C X A X B X C D X × X A + 𝑒 C D X × X B = C D A + 𝑒 C D B
13 5 8 12 3brtr3d M ∞MetSp C X A X B X A D B C D A + 𝑒 C D B