Metamath Proof Explorer

Theorem metdsle

Description: The distance from a point to a set is bounded by the distance to any member of the set. (Contributed by Mario Carneiro, 5-Sep-2015)

Ref Expression
Hypothesis metdscn.f 
|- F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) )
Assertion metdsle 
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. S /\ B e. X ) ) -> ( F ` B ) <_ ( A D B ) )

Proof

Step Hyp Ref Expression
1 metdscn.f 
 |-  F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) )
2 simprr 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. S /\ B e. X ) ) -> B e. X )
3 simpr 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> S C_ X )
4 3 sselda 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ A e. S ) -> A e. X )
5 4 adantrr 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. S /\ B e. X ) ) -> A e. X )
6 2 5 jca 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. S /\ B e. X ) ) -> ( B e. X /\ A e. X ) )
7 1 metdstri 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( B e. X /\ A e. X ) ) -> ( F ` B ) <_ ( ( B D A ) +e ( F ` A ) ) )
8 6 7 syldan 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. S /\ B e. X ) ) -> ( F ` B ) <_ ( ( B D A ) +e ( F ` A ) ) )
9 simpll 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. S /\ B e. X ) ) -> D e. ( *Met ` X ) )
10 xmetsym 
 |-  ( ( D e. ( *Met ` X ) /\ B e. X /\ A e. X ) -> ( B D A ) = ( A D B ) )
11 9 2 5 10 syl3anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. S /\ B e. X ) ) -> ( B D A ) = ( A D B ) )
12 1 metds0 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. S ) -> ( F ` A ) = 0 )
13 12 3expa 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ A e. S ) -> ( F ` A ) = 0 )
14 13 adantrr 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. S /\ B e. X ) ) -> ( F ` A ) = 0 )
15 11 14 oveq12d 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. S /\ B e. X ) ) -> ( ( B D A ) +e ( F ` A ) ) = ( ( A D B ) +e 0 ) )
16 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) e. RR* )
17 9 5 2 16 syl3anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. S /\ B e. X ) ) -> ( A D B ) e. RR* )
18 17 xaddid1d 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. S /\ B e. X ) ) -> ( ( A D B ) +e 0 ) = ( A D B ) )
19 15 18 eqtrd 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. S /\ B e. X ) ) -> ( ( B D A ) +e ( F ` A ) ) = ( A D B ) )
20 8 19 breqtrd 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. S /\ B e. X ) ) -> ( F ` B ) <_ ( A D B ) )