Metamath Proof Explorer

Theorem metrtri

Description: Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 5-May-2014)

Ref Expression
Assertion metrtri ⊢D∈Met⁡X∧A∈X∧B∈X∧C∈X→ADC−BDC≤ADB

Proof

Step Hyp Ref Expression
1 metcl ⊢D∈Met⁡X∧A∈X∧C∈X→ADC∈ℝ
2 1 3adant3r2 ⊢D∈Met⁡X∧A∈X∧B∈X∧C∈X→ADC∈ℝ
3 metcl ⊢D∈Met⁡X∧B∈X∧C∈X→BDC∈ℝ
4 3 3adant3r1 ⊢D∈Met⁡X∧A∈X∧B∈X∧C∈X→BDC∈ℝ
5 eqid ⊢dist⁡ℝ𝑠*=dist⁡ℝ𝑠*
6 5 xrsdsreval ⊢ADC∈ℝ∧BDC∈ℝ→ADCdist⁡ℝ𝑠*BDC=ADC−BDC
7 2 4 6 syl2anc ⊢D∈Met⁡X∧A∈X∧B∈X∧C∈X→ADCdist⁡ℝ𝑠*BDC=ADC−BDC
8 metxmet ⊢D∈Met⁡X→D∈∞Met⁡X
9 5 xmetrtri2 ⊢D∈∞Met⁡X∧A∈X∧B∈X∧C∈X→ADCdist⁡ℝ𝑠*BDC≤ADB
10 8 9 sylan ⊢D∈Met⁡X∧A∈X∧B∈X∧C∈X→ADCdist⁡ℝ𝑠*BDC≤ADB
11 7 10 eqbrtrrd ⊢D∈Met⁡X∧A∈X∧B∈X∧C∈X→ADC−BDC≤ADB