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 ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐶 ) 𝐾 ( 𝐵 𝐷 𝐶 ) ) ≤ ( 𝐴 𝐷 𝐵 ) )