Metamath Proof Explorer

Theorem mettri

Description: Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of Gleason p. 223. (Contributed by NM, 27-Aug-2006)

Ref Expression
Assertion mettri 
|- ( ( D e. ( Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( A D C ) + ( C D B ) ) )

Proof

Step Hyp Ref Expression
1 mettri2 
 |-  ( ( D e. ( Met ` X ) /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( A D B ) <_ ( ( C D A ) + ( C D B ) ) )
2 1 expcom 
 |-  ( ( C e. X /\ A e. X /\ B e. X ) -> ( D e. ( Met ` X ) -> ( A D B ) <_ ( ( C D A ) + ( C D B ) ) ) )
3 2 3coml 
 |-  ( ( A e. X /\ B e. X /\ C e. X ) -> ( D e. ( Met ` X ) -> ( A D B ) <_ ( ( C D A ) + ( C D B ) ) ) )
4 3 impcom 
 |-  ( ( D e. ( Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( C D A ) + ( C D B ) ) )
5 metsym 
 |-  ( ( D e. ( Met ` X ) /\ A e. X /\ C e. X ) -> ( A D C ) = ( C D A ) )
6 5 3adant3r2 
 |-  ( ( D e. ( Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D C ) = ( C D A ) )
7 6 oveq1d 
 |-  ( ( D e. ( Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A D C ) + ( C D B ) ) = ( ( C D A ) + ( C D B ) ) )
8 4 7 breqtrrd 
 |-  ( ( D e. ( Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( A D C ) + ( C D B ) ) )