Metamath Proof Explorer

Theorem mettri2

Description: Triangle inequality for the distance function of a metric space. (Contributed by NM, 30-Aug-2006) (Revised by Mario Carneiro, 20-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
2 xmettri2 
 |-  ( ( D e. ( *Met ` X ) /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( A D B ) <_ ( ( C D A ) +e ( C D B ) ) )
3 1 2 sylan 
 |-  ( ( D e. ( Met ` X ) /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( A D B ) <_ ( ( C D A ) +e ( C D B ) ) )
4 metcl 
 |-  ( ( D e. ( Met ` X ) /\ C e. X /\ A e. X ) -> ( C D A ) e. RR )
5 4 3adant3r3 
 |-  ( ( D e. ( Met ` X ) /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( C D A ) e. RR )
6 metcl 
 |-  ( ( D e. ( Met ` X ) /\ C e. X /\ B e. X ) -> ( C D B ) e. RR )
7 6 3adant3r2 
 |-  ( ( D e. ( Met ` X ) /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( C D B ) e. RR )
8 5 7 rexaddd 
 |-  ( ( D e. ( Met ` X ) /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( ( C D A ) +e ( C D B ) ) = ( ( C D A ) + ( C D B ) ) )
9 3 8 breqtrd 
 |-  ( ( D e. ( Met ` X ) /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( A D B ) <_ ( ( C D A ) + ( C D B ) ) )