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