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

Proof

Step Hyp Ref Expression
1 mettri 
 |-  ( ( D e. ( Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( A D C ) + ( C D B ) ) )
2 metsym 
 |-  ( ( 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 ) + ( B D C ) ) = ( ( A D C ) + ( 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 ) + ( B D C ) ) )