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 𝐾 = ( dist ‘ ℝ*𝑠 )
Assertion xmetrtri2 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐴 𝐷 𝐶 ) 𝐾 ( 𝐵 𝐷 𝐶 ) ) ≤ ( 𝐴 𝐷 𝐵 ) )

Proof

Step Hyp Ref Expression
1 xmetrtri2.1 𝐾 = ( dist ‘ ℝ*𝑠 )
2 xmetcl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴𝑋𝐶𝑋 ) → ( 𝐴 𝐷 𝐶 ) ∈ ℝ* )
3 2 3adant3r2 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( 𝐴 𝐷 𝐶 ) ∈ ℝ* )
4 xmetcl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵𝑋𝐶𝑋 ) → ( 𝐵 𝐷 𝐶 ) ∈ ℝ* )
5 4 3adant3r1 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( 𝐵 𝐷 𝐶 ) ∈ ℝ* )
6 1 xrsdsval ( ( ( 𝐴 𝐷 𝐶 ) ∈ ℝ* ∧ ( 𝐵 𝐷 𝐶 ) ∈ ℝ* ) → ( ( 𝐴 𝐷 𝐶 ) 𝐾 ( 𝐵 𝐷 𝐶 ) ) = if ( ( 𝐴 𝐷 𝐶 ) ≤ ( 𝐵 𝐷 𝐶 ) , ( ( 𝐵 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐶 ) ) , ( ( 𝐴 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐵 𝐷 𝐶 ) ) ) )
7 3 5 6 syl2anc ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐴 𝐷 𝐶 ) 𝐾 ( 𝐵 𝐷 𝐶 ) ) = if ( ( 𝐴 𝐷 𝐶 ) ≤ ( 𝐵 𝐷 𝐶 ) , ( ( 𝐵 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐶 ) ) , ( ( 𝐴 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐵 𝐷 𝐶 ) ) ) )
8 3ancoma ( ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ↔ ( 𝐵𝑋𝐴𝑋𝐶𝑋 ) )
9 xmetrtri ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐵𝑋𝐴𝑋𝐶𝑋 ) ) → ( ( 𝐵 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐶 ) ) ≤ ( 𝐵 𝐷 𝐴 ) )
10 8 9 sylan2b ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐵 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐶 ) ) ≤ ( 𝐵 𝐷 𝐴 ) )
11 xmetsym ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐵 𝐷 𝐴 ) )
12 11 3adant3r3 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐵 𝐷 𝐴 ) )
13 10 12 breqtrrd ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐵 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐶 ) ) ≤ ( 𝐴 𝐷 𝐵 ) )
14 xmetrtri ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐴 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐵 𝐷 𝐶 ) ) ≤ ( 𝐴 𝐷 𝐵 ) )
15 breq1 ( ( ( 𝐵 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐶 ) ) = if ( ( 𝐴 𝐷 𝐶 ) ≤ ( 𝐵 𝐷 𝐶 ) , ( ( 𝐵 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐶 ) ) , ( ( 𝐴 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐵 𝐷 𝐶 ) ) ) → ( ( ( 𝐵 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐶 ) ) ≤ ( 𝐴 𝐷 𝐵 ) ↔ if ( ( 𝐴 𝐷 𝐶 ) ≤ ( 𝐵 𝐷 𝐶 ) , ( ( 𝐵 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐶 ) ) , ( ( 𝐴 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐵 𝐷 𝐶 ) ) ) ≤ ( 𝐴 𝐷 𝐵 ) ) )
16 breq1 ( ( ( 𝐴 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐵 𝐷 𝐶 ) ) = if ( ( 𝐴 𝐷 𝐶 ) ≤ ( 𝐵 𝐷 𝐶 ) , ( ( 𝐵 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐶 ) ) , ( ( 𝐴 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐵 𝐷 𝐶 ) ) ) → ( ( ( 𝐴 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐵 𝐷 𝐶 ) ) ≤ ( 𝐴 𝐷 𝐵 ) ↔ if ( ( 𝐴 𝐷 𝐶 ) ≤ ( 𝐵 𝐷 𝐶 ) , ( ( 𝐵 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐶 ) ) , ( ( 𝐴 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐵 𝐷 𝐶 ) ) ) ≤ ( 𝐴 𝐷 𝐵 ) ) )
17 15 16 ifboth ( ( ( ( 𝐵 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐶 ) ) ≤ ( 𝐴 𝐷 𝐵 ) ∧ ( ( 𝐴 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐵 𝐷 𝐶 ) ) ≤ ( 𝐴 𝐷 𝐵 ) ) → if ( ( 𝐴 𝐷 𝐶 ) ≤ ( 𝐵 𝐷 𝐶 ) , ( ( 𝐵 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐶 ) ) , ( ( 𝐴 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐵 𝐷 𝐶 ) ) ) ≤ ( 𝐴 𝐷 𝐵 ) )
18 13 14 17 syl2anc ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → if ( ( 𝐴 𝐷 𝐶 ) ≤ ( 𝐵 𝐷 𝐶 ) , ( ( 𝐵 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐶 ) ) , ( ( 𝐴 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐵 𝐷 𝐶 ) ) ) ≤ ( 𝐴 𝐷 𝐵 ) )
19 7 18 eqbrtrd ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐴 𝐷 𝐶 ) 𝐾 ( 𝐵 𝐷 𝐶 ) ) ≤ ( 𝐴 𝐷 𝐵 ) )