Metamath Proof Explorer


Theorem xmetrtri

Description: One half of the reverse triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 4-Sep-2015)

Ref Expression
Assertion xmetrtri ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐴 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐵 𝐷 𝐶 ) ) ≤ ( 𝐴 𝐷 𝐵 ) )

Proof

Step Hyp Ref Expression
1 3ancomb ( ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ↔ ( 𝐴𝑋𝐶𝑋𝐵𝑋 ) )
2 xmettri ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐶𝑋𝐵𝑋 ) ) → ( 𝐴 𝐷 𝐶 ) ≤ ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐵 𝐷 𝐶 ) ) )
3 1 2 sylan2b ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( 𝐴 𝐷 𝐶 ) ≤ ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐵 𝐷 𝐶 ) ) )
4 xmetcl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴𝑋𝐶𝑋 ) → ( 𝐴 𝐷 𝐶 ) ∈ ℝ* )
5 4 3adant3r2 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( 𝐴 𝐷 𝐶 ) ∈ ℝ* )
6 xmetcl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵𝑋𝐶𝑋 ) → ( 𝐵 𝐷 𝐶 ) ∈ ℝ* )
7 6 3adant3r1 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( 𝐵 𝐷 𝐶 ) ∈ ℝ* )
8 xmetcl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ* )
9 8 3adant3r3 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ* )
10 xmetge0 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴𝑋𝐶𝑋 ) → 0 ≤ ( 𝐴 𝐷 𝐶 ) )
11 10 3adant3r2 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → 0 ≤ ( 𝐴 𝐷 𝐶 ) )
12 xmetge0 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵𝑋𝐶𝑋 ) → 0 ≤ ( 𝐵 𝐷 𝐶 ) )
13 12 3adant3r1 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → 0 ≤ ( 𝐵 𝐷 𝐶 ) )
14 ge0nemnf ( ( ( 𝐵 𝐷 𝐶 ) ∈ ℝ* ∧ 0 ≤ ( 𝐵 𝐷 𝐶 ) ) → ( 𝐵 𝐷 𝐶 ) ≠ -∞ )
15 7 13 14 syl2anc ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( 𝐵 𝐷 𝐶 ) ≠ -∞ )
16 xmetge0 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴𝑋𝐵𝑋 ) → 0 ≤ ( 𝐴 𝐷 𝐵 ) )
17 16 3adant3r3 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → 0 ≤ ( 𝐴 𝐷 𝐵 ) )
18 xlesubadd ( ( ( ( 𝐴 𝐷 𝐶 ) ∈ ℝ* ∧ ( 𝐵 𝐷 𝐶 ) ∈ ℝ* ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ) ∧ ( 0 ≤ ( 𝐴 𝐷 𝐶 ) ∧ ( 𝐵 𝐷 𝐶 ) ≠ -∞ ∧ 0 ≤ ( 𝐴 𝐷 𝐵 ) ) ) → ( ( ( 𝐴 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐵 𝐷 𝐶 ) ) ≤ ( 𝐴 𝐷 𝐵 ) ↔ ( 𝐴 𝐷 𝐶 ) ≤ ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐵 𝐷 𝐶 ) ) ) )
19 5 7 9 11 15 17 18 syl33anc ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( ( ( 𝐴 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐵 𝐷 𝐶 ) ) ≤ ( 𝐴 𝐷 𝐵 ) ↔ ( 𝐴 𝐷 𝐶 ) ≤ ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐵 𝐷 𝐶 ) ) ) )
20 3 19 mpbird ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐴 𝐷 𝐶 ) +𝑒 -𝑒 ( 𝐵 𝐷 𝐶 ) ) ≤ ( 𝐴 𝐷 𝐵 ) )