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

Proof

Step Hyp Ref Expression
1 3ancomb ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) )
2 xmettri ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐶 ) ≤ ( ( 𝐴 𝐷 𝐵 ) +e ( 𝐵 𝐷 𝐶 ) ) )
3 1 2 sylan2b ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐶 ) ≤ ( ( 𝐴 𝐷 𝐵 ) +e ( 𝐵 𝐷 𝐶 ) ) )
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 ≤ ( 𝐴 𝐷 𝐵 ) ) ) → ( ( ( 𝐴 𝐷 𝐶 ) +e -e ( 𝐵 𝐷 𝐶 ) ) ≤ ( 𝐴 𝐷 𝐵 ) ↔ ( 𝐴 𝐷 𝐶 ) ≤ ( ( 𝐴 𝐷 𝐵 ) +e ( 𝐵 𝐷 𝐶 ) ) ) )
19 5 7 9 11 15 17 18 syl33anc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( ( 𝐴 𝐷 𝐶 ) +e -e ( 𝐵 𝐷 𝐶 ) ) ≤ ( 𝐴 𝐷 𝐵 ) ↔ ( 𝐴 𝐷 𝐶 ) ≤ ( ( 𝐴 𝐷 𝐵 ) +e ( 𝐵 𝐷 𝐶 ) ) ) )
20 3 19 mpbird ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐶 ) +e -e ( 𝐵 𝐷 𝐶 ) ) ≤ ( 𝐴 𝐷 𝐵 ) )