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 
|- ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( A D C ) +e ( B D C ) ) )

Proof

Step Hyp Ref Expression
1 xmettri 
 |-  ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( A D C ) +e ( C D B ) ) )
2 xmetsym 
 |-  ( ( D e. ( *Met ` X ) /\ B e. X /\ C e. X ) -> ( B D C ) = ( C D B ) )
3 2 3adant3r1 
 |-  ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( B D C ) = ( C D B ) )
4 3 oveq2d 
 |-  ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A D C ) +e ( B D C ) ) = ( ( A D C ) +e ( C D B ) ) )
5 1 4 breqtrrd 
 |-  ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( A D C ) +e ( B D C ) ) )