Metamath Proof Explorer

Theorem xmetrtri2

Description: The reverse triangle inequality for the distance function of an extended metric. In order to express the "extended absolute value function", we use the distance function xrsdsval defined on the extended real structure. (Contributed by Mario Carneiro, 4-Sep-2015)

Ref Expression
Hypothesis xmetrtri2.1 ⊒K=dist⁑ℝ𝑠*
Assertion xmetrtri2 ⊒D∈∞Met⁑X∧A∈X∧B∈X∧C∈Xβ†’ADCKBDC≀ADB

Proof

Step Hyp Ref Expression
1 xmetrtri2.1 ⊒K=dist⁑ℝ𝑠*
2 xmetcl ⊒D∈∞Met⁑X∧A∈X∧C∈Xβ†’ADCβˆˆβ„*
3 2 3adant3r2 ⊒D∈∞Met⁑X∧A∈X∧B∈X∧C∈Xβ†’ADCβˆˆβ„*
4 xmetcl ⊒D∈∞Met⁑X∧B∈X∧C∈Xβ†’BDCβˆˆβ„*
5 4 3adant3r1 ⊒D∈∞Met⁑X∧A∈X∧B∈X∧C∈Xβ†’BDCβˆˆβ„*
6 1 xrsdsval ⊒ADCβˆˆβ„*∧BDCβˆˆβ„*β†’ADCKBDC=ifADC≀BDCBDC+π‘’βˆ’ADCADC+π‘’βˆ’BDC
7 3 5 6 syl2anc ⊒D∈∞Met⁑X∧A∈X∧B∈X∧C∈Xβ†’ADCKBDC=ifADC≀BDCBDC+π‘’βˆ’ADCADC+π‘’βˆ’BDC
8 3ancoma ⊒A∈X∧B∈X∧C∈X↔B∈X∧A∈X∧C∈X
9 xmetrtri ⊒D∈∞Met⁑X∧B∈X∧A∈X∧C∈Xβ†’BDC+π‘’βˆ’ADC≀BDA
10 8 9 sylan2b ⊒D∈∞Met⁑X∧A∈X∧B∈X∧C∈Xβ†’BDC+π‘’βˆ’ADC≀BDA
11 xmetsym ⊒D∈∞Met⁑X∧A∈X∧B∈Xβ†’ADB=BDA
12 11 3adant3r3 ⊒D∈∞Met⁑X∧A∈X∧B∈X∧C∈Xβ†’ADB=BDA
13 10 12 breqtrrd ⊒D∈∞Met⁑X∧A∈X∧B∈X∧C∈Xβ†’BDC+π‘’βˆ’ADC≀ADB
14 xmetrtri ⊒D∈∞Met⁑X∧A∈X∧B∈X∧C∈Xβ†’ADC+π‘’βˆ’BDC≀ADB
15 breq1 ⊒BDC+π‘’βˆ’ADC=ifADC≀BDCBDC+π‘’βˆ’ADCADC+π‘’βˆ’BDCβ†’BDC+π‘’βˆ’ADC≀ADB↔ifADC≀BDCBDC+π‘’βˆ’ADCADC+π‘’βˆ’BDC≀ADB
16 breq1 ⊒ADC+π‘’βˆ’BDC=ifADC≀BDCBDC+π‘’βˆ’ADCADC+π‘’βˆ’BDCβ†’ADC+π‘’βˆ’BDC≀ADB↔ifADC≀BDCBDC+π‘’βˆ’ADCADC+π‘’βˆ’BDC≀ADB
17 15 16 ifboth ⊒BDC+π‘’βˆ’ADC≀ADB∧ADC+π‘’βˆ’BDC≀ADBβ†’ifADC≀BDCBDC+π‘’βˆ’ADCADC+π‘’βˆ’BDC≀ADB
18 13 14 17 syl2anc ⊒D∈∞Met⁑X∧A∈X∧B∈X∧C∈Xβ†’ifADC≀BDCBDC+π‘’βˆ’ADCADC+π‘’βˆ’BDC≀ADB
19 7 18 eqbrtrd ⊒D∈∞Met⁑X∧A∈X∧B∈X∧C∈Xβ†’ADCKBDC≀ADB