This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem metrtri

Description: Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 5-May-2014)

		Ref	Expression
	Assertion	metrtri	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( abs ‘ ( ( 𝐴 𝐷 𝐶 ) − ( 𝐵 𝐷 𝐶 ) ) ) ≤ ( 𝐴 𝐷 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		metcl	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐶 ) ∈ ℝ )
2	1	3adant3r2	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐶 ) ∈ ℝ )
3		metcl	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 𝐷 𝐶 ) ∈ ℝ )
4	3	3adant3r1	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 𝐷 𝐶 ) ∈ ℝ )
5		eqid	⊢ ( dist ‘ ℝ^_𝑠 ) = ( dist ‘ ℝ^_𝑠 )
6	5	xrsdsreval	⊢ ( ( ( 𝐴 𝐷 𝐶 ) ∈ ℝ ∧ ( 𝐵 𝐷 𝐶 ) ∈ ℝ ) → ( ( 𝐴 𝐷 𝐶 ) ( dist ‘ ℝ^*_𝑠 ) ( 𝐵 𝐷 𝐶 ) ) = ( abs ‘ ( ( 𝐴 𝐷 𝐶 ) − ( 𝐵 𝐷 𝐶 ) ) ) )
7	2 4 6	syl2anc	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐶 ) ( dist ‘ ℝ^*_𝑠 ) ( 𝐵 𝐷 𝐶 ) ) = ( abs ‘ ( ( 𝐴 𝐷 𝐶 ) − ( 𝐵 𝐷 𝐶 ) ) ) )
8		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
9	5	xmetrtri2	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐶 ) ( dist ‘ ℝ^*_𝑠 ) ( 𝐵 𝐷 𝐶 ) ) ≤ ( 𝐴 𝐷 𝐵 ) )
10	8 9	sylan	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐶 ) ( dist ‘ ℝ^*_𝑠 ) ( 𝐵 𝐷 𝐶 ) ) ≤ ( 𝐴 𝐷 𝐵 ) )
11	7 10	eqbrtrrd	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( abs ‘ ( ( 𝐴 𝐷 𝐶 ) − ( 𝐵 𝐷 𝐶 ) ) ) ≤ ( 𝐴 𝐷 𝐵 ) )