Metamath Proof Explorer

Theorem msrtri

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

Ref Expression
Hypotheses mscl.x ⊢X=BaseM
mscl.d ⊢D=dist⁡M
Assertion msrtri ⊢M∈MetSp∧A∈X∧B∈X∧C∈X→ADC−BDC≤ADB

Proof

Step Hyp Ref Expression
1 mscl.x ⊢X=BaseM
2 mscl.d ⊢D=dist⁡M
3 1 2 msmet2 ⊢M∈MetSp→D↾X×X∈Met⁡X
4 metrtri ⊢D↾X×X∈Met⁡X∧A∈X∧B∈X∧C∈X→AD↾X×XC−BD↾X×XC≤AD↾X×XB
5 3 4 sylan ⊢M∈MetSp∧A∈X∧B∈X∧C∈X→AD↾X×XC−BD↾X×XC≤AD↾X×XB
6 simpr1 ⊢M∈MetSp∧A∈X∧B∈X∧C∈X→A∈X
7 simpr3 ⊢M∈MetSp∧A∈X∧B∈X∧C∈X→C∈X
8 6 7 ovresd ⊢M∈MetSp∧A∈X∧B∈X∧C∈X→AD↾X×XC=ADC
9 simpr2 ⊢M∈MetSp∧A∈X∧B∈X∧C∈X→B∈X
10 9 7 ovresd ⊢M∈MetSp∧A∈X∧B∈X∧C∈X→BD↾X×XC=BDC
11 8 10 oveq12d ⊢M∈MetSp∧A∈X∧B∈X∧C∈X→AD↾X×XC−BD↾X×XC=ADC−BDC
12 11 fveq2d ⊢M∈MetSp∧A∈X∧B∈X∧C∈X→AD↾X×XC−BD↾X×XC=ADC−BDC
13 6 9 ovresd ⊢M∈MetSp∧A∈X∧B∈X∧C∈X→AD↾X×XB=ADB
14 5 12 13 3brtr3d ⊢M∈MetSp∧A∈X∧B∈X∧C∈X→ADC−BDC≤ADB