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