Metamath Proof Explorer

Theorem xmettri2

Description: Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 elfvdm 
 |-  ( D e. ( *Met ` X ) -> X e. dom *Met )
2 isxmet 
 |-  ( X e. dom *Met -> ( D e. ( *Met ` X ) <-> ( D : ( X X. X ) --> RR* /\ A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) )
3 1 2 syl 
 |-  ( D e. ( *Met ` X ) -> ( D e. ( *Met ` X ) <-> ( D : ( X X. X ) --> RR* /\ A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) )
4 3 ibi 
 |-  ( D e. ( *Met ` X ) -> ( D : ( X X. X ) --> RR* /\ A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) )
5 simpr 
 |-  ( ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) -> A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )
6 5 2ralimi 
 |-  ( A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) -> A. x e. X A. y e. X A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )
7 4 6 simpl2im 
 |-  ( D e. ( *Met ` X ) -> A. x e. X A. y e. X A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )
8 oveq1 
 |-  ( x = A -> ( x D y ) = ( A D y ) )
9 oveq2 
 |-  ( x = A -> ( z D x ) = ( z D A ) )
10 9 oveq1d 
 |-  ( x = A -> ( ( z D x ) +e ( z D y ) ) = ( ( z D A ) +e ( z D y ) ) )
11 8 10 breq12d 
 |-  ( x = A -> ( ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) <-> ( A D y ) <_ ( ( z D A ) +e ( z D y ) ) ) )
12 oveq2 
 |-  ( y = B -> ( A D y ) = ( A D B ) )
13 oveq2 
 |-  ( y = B -> ( z D y ) = ( z D B ) )
14 13 oveq2d 
 |-  ( y = B -> ( ( z D A ) +e ( z D y ) ) = ( ( z D A ) +e ( z D B ) ) )
15 12 14 breq12d 
 |-  ( y = B -> ( ( A D y ) <_ ( ( z D A ) +e ( z D y ) ) <-> ( A D B ) <_ ( ( z D A ) +e ( z D B ) ) ) )
16 oveq1 
 |-  ( z = C -> ( z D A ) = ( C D A ) )
17 oveq1 
 |-  ( z = C -> ( z D B ) = ( C D B ) )
18 16 17 oveq12d 
 |-  ( z = C -> ( ( z D A ) +e ( z D B ) ) = ( ( C D A ) +e ( C D B ) ) )
19 18 breq2d 
 |-  ( z = C -> ( ( A D B ) <_ ( ( z D A ) +e ( z D B ) ) <-> ( A D B ) <_ ( ( C D A ) +e ( C D B ) ) ) )
20 11 15 19 rspc3v 
 |-  ( ( A e. X /\ B e. X /\ C e. X ) -> ( A. x e. X A. y e. X A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) -> ( A D B ) <_ ( ( C D A ) +e ( C D B ) ) ) )
21 7 20 syl5 
 |-  ( ( A e. X /\ B e. X /\ C e. X ) -> ( D e. ( *Met ` X ) -> ( A D B ) <_ ( ( C D A ) +e ( C D B ) ) ) )
22 21 3comr 
 |-  ( ( C e. X /\ A e. X /\ B e. X ) -> ( D e. ( *Met ` X ) -> ( A D B ) <_ ( ( C D A ) +e ( C D B ) ) ) )
23 22 impcom 
 |-  ( ( D e. ( *Met ` X ) /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( A D B ) <_ ( ( C D A ) +e ( C D B ) ) )