Metamath Proof Explorer

Theorem metdscnlem

Description: Lemma for metdscn . (Contributed by Mario Carneiro, 4-Sep-2015)

Ref Expression
Hypotheses metdscn.f 
|- F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) )
metdscn.j 
|- J = ( MetOpen ` D )
metdscn.c 
|- C = ( dist ` RR*s )
metdscn.k 
|- K = ( MetOpen ` C )
metdscnlem.1 
|- ( ph -> D e. ( *Met ` X ) )
metdscnlem.2 
|- ( ph -> S C_ X )
metdscnlem.3 
|- ( ph -> A e. X )
metdscnlem.4 
|- ( ph -> B e. X )
metdscnlem.5 
|- ( ph -> R e. RR+ )
metdscnlem.6 
|- ( ph -> ( A D B ) < R )
Assertion metdscnlem 
|- ( ph -> ( ( F ` A ) +e -e ( F ` B ) ) < R )

Proof

Step Hyp Ref Expression
1 metdscn.f 
 |-  F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) )
2 metdscn.j 
 |-  J = ( MetOpen ` D )
3 metdscn.c 
 |-  C = ( dist ` RR*s )
4 metdscn.k 
 |-  K = ( MetOpen ` C )
5 metdscnlem.1 
 |-  ( ph -> D e. ( *Met ` X ) )
6 metdscnlem.2 
 |-  ( ph -> S C_ X )
7 metdscnlem.3 
 |-  ( ph -> A e. X )
8 metdscnlem.4 
 |-  ( ph -> B e. X )
9 metdscnlem.5 
 |-  ( ph -> R e. RR+ )
10 metdscnlem.6 
 |-  ( ph -> ( A D B ) < R )
11 1 metdsf 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> F : X --> ( 0 [,] +oo ) )
12 5 6 11 syl2anc 
 |-  ( ph -> F : X --> ( 0 [,] +oo ) )
13 12 7 ffvelcdmd 
 |-  ( ph -> ( F ` A ) e. ( 0 [,] +oo ) )
14 eliccxr 
 |-  ( ( F ` A ) e. ( 0 [,] +oo ) -> ( F ` A ) e. RR* )
15 13 14 syl 
 |-  ( ph -> ( F ` A ) e. RR* )
16 12 8 ffvelcdmd 
 |-  ( ph -> ( F ` B ) e. ( 0 [,] +oo ) )
17 eliccxr 
 |-  ( ( F ` B ) e. ( 0 [,] +oo ) -> ( F ` B ) e. RR* )
18 16 17 syl 
 |-  ( ph -> ( F ` B ) e. RR* )
19 18 xnegcld 
 |-  ( ph -> -e ( F ` B ) e. RR* )
20 15 19 xaddcld 
 |-  ( ph -> ( ( F ` A ) +e -e ( F ` B ) ) e. RR* )
21 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) e. RR* )
22 5 7 8 21 syl3anc 
 |-  ( ph -> ( A D B ) e. RR* )
23 9 rpxrd 
 |-  ( ph -> R e. RR* )
24 1 metdstri 
 |-  ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( F ` A ) <_ ( ( A D B ) +e ( F ` B ) ) )
25 5 6 7 8 24 syl22anc 
 |-  ( ph -> ( F ` A ) <_ ( ( A D B ) +e ( F ` B ) ) )
26 elxrge0 
 |-  ( ( F ` A ) e. ( 0 [,] +oo ) <-> ( ( F ` A ) e. RR* /\ 0 <_ ( F ` A ) ) )
27 26 simprbi 
 |-  ( ( F ` A ) e. ( 0 [,] +oo ) -> 0 <_ ( F ` A ) )
28 13 27 syl 
 |-  ( ph -> 0 <_ ( F ` A ) )
29 elxrge0 
 |-  ( ( F ` B ) e. ( 0 [,] +oo ) <-> ( ( F ` B ) e. RR* /\ 0 <_ ( F ` B ) ) )
30 29 simprbi 
 |-  ( ( F ` B ) e. ( 0 [,] +oo ) -> 0 <_ ( F ` B ) )
31 16 30 syl 
 |-  ( ph -> 0 <_ ( F ` B ) )
32 ge0nemnf 
 |-  ( ( ( F ` B ) e. RR* /\ 0 <_ ( F ` B ) ) -> ( F ` B ) =/= -oo )
33 18 31 32 syl2anc 
 |-  ( ph -> ( F ` B ) =/= -oo )
34 xmetge0 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> 0 <_ ( A D B ) )
35 5 7 8 34 syl3anc 
 |-  ( ph -> 0 <_ ( A D B ) )
36 xlesubadd 
 |-  ( ( ( ( F ` A ) e. RR* /\ ( F ` B ) e. RR* /\ ( A D B ) e. RR* ) /\ ( 0 <_ ( F ` A ) /\ ( F ` B ) =/= -oo /\ 0 <_ ( A D B ) ) ) -> ( ( ( F ` A ) +e -e ( F ` B ) ) <_ ( A D B ) <-> ( F ` A ) <_ ( ( A D B ) +e ( F ` B ) ) ) )
37 15 18 22 28 33 35 36 syl33anc 
 |-  ( ph -> ( ( ( F ` A ) +e -e ( F ` B ) ) <_ ( A D B ) <-> ( F ` A ) <_ ( ( A D B ) +e ( F ` B ) ) ) )
38 25 37 mpbird 
 |-  ( ph -> ( ( F ` A ) +e -e ( F ` B ) ) <_ ( A D B ) )
39 20 22 23 38 10 xrlelttrd 
 |-  ( ph -> ( ( F ` A ) +e -e ( F ` B ) ) < R )