Metamath Proof Explorer

Theorem xmetrtri

Description: One half of the reverse triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 4-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 3ancomb 
 |-  ( ( A e. X /\ B e. X /\ C e. X ) <-> ( A e. X /\ C e. X /\ B e. X ) )
2 xmettri 
 |-  ( ( D e. ( *Met ` X ) /\ ( A e. X /\ C e. X /\ B e. X ) ) -> ( A D C ) <_ ( ( A D B ) +e ( B D C ) ) )
3 1 2 sylan2b 
 |-  ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D C ) <_ ( ( A D B ) +e ( B D C ) ) )
4 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ C e. X ) -> ( A D C ) e. RR* )
5 4 3adant3r2 
 |-  ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D C ) e. RR* )
6 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ B e. X /\ C e. X ) -> ( B D C ) e. RR* )
7 6 3adant3r1 
 |-  ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( B D C ) e. RR* )
8 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) e. RR* )
9 8 3adant3r3 
 |-  ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) e. RR* )
10 xmetge0 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ C e. X ) -> 0 <_ ( A D C ) )
11 10 3adant3r2 
 |-  ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> 0 <_ ( A D C ) )
12 xmetge0 
 |-  ( ( D e. ( *Met ` X ) /\ B e. X /\ C e. X ) -> 0 <_ ( B D C ) )
13 12 3adant3r1 
 |-  ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> 0 <_ ( B D C ) )
14 ge0nemnf 
 |-  ( ( ( B D C ) e. RR* /\ 0 <_ ( B D C ) ) -> ( B D C ) =/= -oo )
15 7 13 14 syl2anc 
 |-  ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( B D C ) =/= -oo )
16 xmetge0 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> 0 <_ ( A D B ) )
17 16 3adant3r3 
 |-  ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> 0 <_ ( A D B ) )
18 xlesubadd 
 |-  ( ( ( ( A D C ) e. RR* /\ ( B D C ) e. RR* /\ ( A D B ) e. RR* ) /\ ( 0 <_ ( A D C ) /\ ( B D C ) =/= -oo /\ 0 <_ ( A D B ) ) ) -> ( ( ( A D C ) +e -e ( B D C ) ) <_ ( A D B ) <-> ( A D C ) <_ ( ( A D B ) +e ( B D C ) ) ) )
19 5 7 9 11 15 17 18 syl33anc 
 |-  ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( ( A D C ) +e -e ( B D C ) ) <_ ( A D B ) <-> ( A D C ) <_ ( ( A D B ) +e ( B D C ) ) ) )
20 3 19 mpbird 
 |-  ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A D C ) +e -e ( B D C ) ) <_ ( A D B ) )