Metamath Proof Explorer


Theorem mstri

Description: Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of Gleason p. 223. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses mscl.x X=BaseM
mscl.d D=distM
Assertion mstri MMetSpAXBXCXADBADC+CDB

Proof

Step Hyp Ref Expression
1 mscl.x X=BaseM
2 mscl.d D=distM
3 1 2 msmet2 MMetSpDX×XMetX
4 mettri DX×XMetXAXBXCXADX×XBADX×XC+CDX×XB
5 3 4 sylan MMetSpAXBXCXADX×XBADX×XC+CDX×XB
6 simpr1 MMetSpAXBXCXAX
7 simpr2 MMetSpAXBXCXBX
8 6 7 ovresd MMetSpAXBXCXADX×XB=ADB
9 simpr3 MMetSpAXBXCXCX
10 6 9 ovresd MMetSpAXBXCXADX×XC=ADC
11 9 7 ovresd MMetSpAXBXCXCDX×XB=CDB
12 10 11 oveq12d MMetSpAXBXCXADX×XC+CDX×XB=ADC+CDB
13 5 8 12 3brtr3d MMetSpAXBXCXADBADC+CDB