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

Metamath Proof Explorer

Theorem mettri3

Description: Triangle inequality for the distance function of a metric space. (Contributed by NM, 13-Mar-2007)

Ref Expression
Assertion mettri3 ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) ≤ ( ( 𝐴 𝐷 𝐶 ) + ( 𝐵 𝐷 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 mettri ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) ≤ ( ( 𝐴 𝐷 𝐶 ) + ( 𝐶 𝐷 𝐵 ) ) )
2 metsym ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 𝐷 𝐶 ) = ( 𝐶 𝐷 𝐵 ) )
3 2 3adant3r1 ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 𝐷 𝐶 ) = ( 𝐶 𝐷 𝐵 ) )
4 3 oveq2d ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐶 ) + ( 𝐵 𝐷 𝐶 ) ) = ( ( 𝐴 𝐷 𝐶 ) + ( 𝐶 𝐷 𝐵 ) ) )
5 1 4 breqtrrd ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) ≤ ( ( 𝐴 𝐷 𝐶 ) + ( 𝐵 𝐷 𝐶 ) ) )