Metamath Proof Explorer


Theorem xmettri3

Description: Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 xmettri ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) ≤ ( ( 𝐴 𝐷 𝐶 ) +𝑒 ( 𝐶 𝐷 𝐵 ) ) )
2 xmetsym ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵𝑋𝐶𝑋 ) → ( 𝐵 𝐷 𝐶 ) = ( 𝐶 𝐷 𝐵 ) )
3 2 3adant3r1 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( 𝐵 𝐷 𝐶 ) = ( 𝐶 𝐷 𝐵 ) )
4 3 oveq2d ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐴 𝐷 𝐶 ) +𝑒 ( 𝐵 𝐷 𝐶 ) ) = ( ( 𝐴 𝐷 𝐶 ) +𝑒 ( 𝐶 𝐷 𝐵 ) ) )
5 1 4 breqtrrd ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) ≤ ( ( 𝐴 𝐷 𝐶 ) +𝑒 ( 𝐵 𝐷 𝐶 ) ) )