Metamath Proof Explorer

Theorem metrtri

Description: Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 5-May-2014)

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

Proof

Step Hyp Ref Expression
1 metcl 
 |-  ( ( D e. ( Met ` X ) /\ A e. X /\ C e. X ) -> ( A D C ) e. RR )
2 1 3adant3r2 
 |-  ( ( D e. ( Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D C ) e. RR )
3 metcl 
 |-  ( ( D e. ( Met ` X ) /\ B e. X /\ C e. X ) -> ( B D C ) e. RR )
4 3 3adant3r1 
 |-  ( ( D e. ( Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( B D C ) e. RR )
5 eqid 
 |-  ( dist ` RR*s ) = ( dist ` RR*s )
6 5 xrsdsreval 
 |-  ( ( ( A D C ) e. RR /\ ( B D C ) e. RR ) -> ( ( A D C ) ( dist ` RR*s ) ( B D C ) ) = ( abs ` ( ( A D C ) - ( B D C ) ) ) )
7 2 4 6 syl2anc 
 |-  ( ( D e. ( Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A D C ) ( dist ` RR*s ) ( B D C ) ) = ( abs ` ( ( A D C ) - ( B D C ) ) ) )
8 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
9 5 xmetrtri2 
 |-  ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A D C ) ( dist ` RR*s ) ( B D C ) ) <_ ( A D B ) )
10 8 9 sylan 
 |-  ( ( D e. ( Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A D C ) ( dist ` RR*s ) ( B D C ) ) <_ ( A D B ) )
11 7 10 eqbrtrrd 
 |-  ( ( D e. ( Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( abs ` ( ( A D C ) - ( B D C ) ) ) <_ ( A D B ) )