Metamath Proof Explorer


Theorem mstri3

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

Ref Expression
Hypotheses mscl.x X = Base M
mscl.d D = dist M
Assertion mstri3 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 msmet2 M MetSp D X × X Met X
4 mettri3 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