Metamath Proof Explorer

Theorem lebnumlem1

Description: Lemma for lebnum . The function F measures the sum of all of the distances to escape the sets of the cover. Since by assumption it is a cover, there is at least one set which covers a given point, and since it is open, the point is a positive distance from the edge of the set. Thus, the sum is a strictly positive number. (Contributed by Mario Carneiro, 14-Feb-2015) (Revised by AV, 30-Sep-2020)

Ref Expression
Hypotheses lebnum.j 
|- J = ( MetOpen ` D )
lebnum.d 
|- ( ph -> D e. ( Met ` X ) )
lebnum.c 
|- ( ph -> J e. Comp )
lebnum.s 
|- ( ph -> U C_ J )
lebnum.u 
|- ( ph -> X = U. U )
lebnumlem1.u 
|- ( ph -> U e. Fin )
lebnumlem1.n 
|- ( ph -> -. X e. U )
lebnumlem1.f 
|- F = ( y e. X |-> sum_ k e. U inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) )
Assertion lebnumlem1 
|- ( ph -> F : X --> RR+ )

Proof

Step Hyp Ref Expression
1 lebnum.j 
 |-  J = ( MetOpen ` D )
2 lebnum.d 
 |-  ( ph -> D e. ( Met ` X ) )
3 lebnum.c 
 |-  ( ph -> J e. Comp )
4 lebnum.s 
 |-  ( ph -> U C_ J )
5 lebnum.u 
 |-  ( ph -> X = U. U )
6 lebnumlem1.u 
 |-  ( ph -> U e. Fin )
7 lebnumlem1.n 
 |-  ( ph -> -. X e. U )
8 lebnumlem1.f 
 |-  F = ( y e. X |-> sum_ k e. U inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) )
9 6 adantr 
 |-  ( ( ph /\ y e. X ) -> U e. Fin )
10 2 ad2antrr 
 |-  ( ( ( ph /\ y e. X ) /\ k e. U ) -> D e. ( Met ` X ) )
11 difssd 
 |-  ( ( ( ph /\ y e. X ) /\ k e. U ) -> ( X \ k ) C_ X )
12 4 adantr 
 |-  ( ( ph /\ y e. X ) -> U C_ J )
13 12 sselda 
 |-  ( ( ( ph /\ y e. X ) /\ k e. U ) -> k e. J )
14 elssuni 
 |-  ( k e. J -> k C_ U. J )
15 13 14 syl 
 |-  ( ( ( ph /\ y e. X ) /\ k e. U ) -> k C_ U. J )
16 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
17 2 16 syl 
 |-  ( ph -> D e. ( *Met ` X ) )
18 1 mopnuni 
 |-  ( D e. ( *Met ` X ) -> X = U. J )
19 17 18 syl 
 |-  ( ph -> X = U. J )
20 19 ad2antrr 
 |-  ( ( ( ph /\ y e. X ) /\ k e. U ) -> X = U. J )
21 15 20 sseqtrrd 
 |-  ( ( ( ph /\ y e. X ) /\ k e. U ) -> k C_ X )
22 eleq1 
 |-  ( k = X -> ( k e. U <-> X e. U ) )
23 22 notbid 
 |-  ( k = X -> ( -. k e. U <-> -. X e. U ) )
24 7 23 syl5ibrcom 
 |-  ( ph -> ( k = X -> -. k e. U ) )
25 24 necon2ad 
 |-  ( ph -> ( k e. U -> k =/= X ) )
26 25 adantr 
 |-  ( ( ph /\ y e. X ) -> ( k e. U -> k =/= X ) )
27 26 imp 
 |-  ( ( ( ph /\ y e. X ) /\ k e. U ) -> k =/= X )
28 pssdifn0 
 |-  ( ( k C_ X /\ k =/= X ) -> ( X \ k ) =/= (/) )
29 21 27 28 syl2anc 
 |-  ( ( ( ph /\ y e. X ) /\ k e. U ) -> ( X \ k ) =/= (/) )
30 eqid 
 |-  ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) = ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) )
31 30 metdsre 
 |-  ( ( D e. ( Met ` X ) /\ ( X \ k ) C_ X /\ ( X \ k ) =/= (/) ) -> ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) : X --> RR )
32 10 11 29 31 syl3anc 
 |-  ( ( ( ph /\ y e. X ) /\ k e. U ) -> ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) : X --> RR )
33 30 fmpt 
 |-  ( A. y e. X inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) e. RR <-> ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) : X --> RR )
34 32 33 sylibr 
 |-  ( ( ( ph /\ y e. X ) /\ k e. U ) -> A. y e. X inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) e. RR )
35 simplr 
 |-  ( ( ( ph /\ y e. X ) /\ k e. U ) -> y e. X )
36 rsp 
 |-  ( A. y e. X inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) e. RR -> ( y e. X -> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) e. RR ) )
37 34 35 36 sylc 
 |-  ( ( ( ph /\ y e. X ) /\ k e. U ) -> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) e. RR )
38 9 37 fsumrecl 
 |-  ( ( ph /\ y e. X ) -> sum_ k e. U inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) e. RR )
39 5 eleq2d 
 |-  ( ph -> ( y e. X <-> y e. U. U ) )
40 39 biimpa 
 |-  ( ( ph /\ y e. X ) -> y e. U. U )
41 eluni2 
 |-  ( y e. U. U <-> E. m e. U y e. m )
42 40 41 sylib 
 |-  ( ( ph /\ y e. X ) -> E. m e. U y e. m )
43 0red 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> 0 e. RR )
44 simplr 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> y e. X )
45 eqid 
 |-  ( w e. X |-> inf ( ran ( z e. ( X \ m ) |-> ( w D z ) ) , RR* , < ) ) = ( w e. X |-> inf ( ran ( z e. ( X \ m ) |-> ( w D z ) ) , RR* , < ) )
46 45 metdsval 
 |-  ( y e. X -> ( ( w e. X |-> inf ( ran ( z e. ( X \ m ) |-> ( w D z ) ) , RR* , < ) ) ` y ) = inf ( ran ( z e. ( X \ m ) |-> ( y D z ) ) , RR* , < ) )
47 44 46 syl 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> ( ( w e. X |-> inf ( ran ( z e. ( X \ m ) |-> ( w D z ) ) , RR* , < ) ) ` y ) = inf ( ran ( z e. ( X \ m ) |-> ( y D z ) ) , RR* , < ) )
48 2 ad2antrr 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> D e. ( Met ` X ) )
49 difssd 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> ( X \ m ) C_ X )
50 4 ad2antrr 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> U C_ J )
51 simprl 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> m e. U )
52 50 51 sseldd 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> m e. J )
53 elssuni 
 |-  ( m e. J -> m C_ U. J )
54 52 53 syl 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> m C_ U. J )
55 48 16 18 3syl 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> X = U. J )
56 54 55 sseqtrrd 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> m C_ X )
57 eleq1 
 |-  ( m = X -> ( m e. U <-> X e. U ) )
58 57 notbid 
 |-  ( m = X -> ( -. m e. U <-> -. X e. U ) )
59 7 58 syl5ibrcom 
 |-  ( ph -> ( m = X -> -. m e. U ) )
60 59 necon2ad 
 |-  ( ph -> ( m e. U -> m =/= X ) )
61 60 ad2antrr 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> ( m e. U -> m =/= X ) )
62 51 61 mpd 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> m =/= X )
63 pssdifn0 
 |-  ( ( m C_ X /\ m =/= X ) -> ( X \ m ) =/= (/) )
64 56 62 63 syl2anc 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> ( X \ m ) =/= (/) )
65 45 metdsre 
 |-  ( ( D e. ( Met ` X ) /\ ( X \ m ) C_ X /\ ( X \ m ) =/= (/) ) -> ( w e. X |-> inf ( ran ( z e. ( X \ m ) |-> ( w D z ) ) , RR* , < ) ) : X --> RR )
66 48 49 64 65 syl3anc 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> ( w e. X |-> inf ( ran ( z e. ( X \ m ) |-> ( w D z ) ) , RR* , < ) ) : X --> RR )
67 66 44 ffvelrnd 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> ( ( w e. X |-> inf ( ran ( z e. ( X \ m ) |-> ( w D z ) ) , RR* , < ) ) ` y ) e. RR )
68 47 67 eqeltrrd 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> inf ( ran ( z e. ( X \ m ) |-> ( y D z ) ) , RR* , < ) e. RR )
69 38 adantr 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> sum_ k e. U inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) e. RR )
70 17 ad2antrr 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> D e. ( *Met ` X ) )
71 45 metdsf 
 |-  ( ( D e. ( *Met ` X ) /\ ( X \ m ) C_ X ) -> ( w e. X |-> inf ( ran ( z e. ( X \ m ) |-> ( w D z ) ) , RR* , < ) ) : X --> ( 0 [,] +oo ) )
72 70 49 71 syl2anc 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> ( w e. X |-> inf ( ran ( z e. ( X \ m ) |-> ( w D z ) ) , RR* , < ) ) : X --> ( 0 [,] +oo ) )
73 72 44 ffvelrnd 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> ( ( w e. X |-> inf ( ran ( z e. ( X \ m ) |-> ( w D z ) ) , RR* , < ) ) ` y ) e. ( 0 [,] +oo ) )
74 elxrge0 
 |-  ( ( ( w e. X |-> inf ( ran ( z e. ( X \ m ) |-> ( w D z ) ) , RR* , < ) ) ` y ) e. ( 0 [,] +oo ) <-> ( ( ( w e. X |-> inf ( ran ( z e. ( X \ m ) |-> ( w D z ) ) , RR* , < ) ) ` y ) e. RR* /\ 0 <_ ( ( w e. X |-> inf ( ran ( z e. ( X \ m ) |-> ( w D z ) ) , RR* , < ) ) ` y ) ) )
75 73 74 sylib 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> ( ( ( w e. X |-> inf ( ran ( z e. ( X \ m ) |-> ( w D z ) ) , RR* , < ) ) ` y ) e. RR* /\ 0 <_ ( ( w e. X |-> inf ( ran ( z e. ( X \ m ) |-> ( w D z ) ) , RR* , < ) ) ` y ) ) )
76 75 simprd 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> 0 <_ ( ( w e. X |-> inf ( ran ( z e. ( X \ m ) |-> ( w D z ) ) , RR* , < ) ) ` y ) )
77 elndif 
 |-  ( y e. m -> -. y e. ( X \ m ) )
78 77 ad2antll 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> -. y e. ( X \ m ) )
79 55 difeq1d 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> ( X \ m ) = ( U. J \ m ) )
80 1 mopntop 
 |-  ( D e. ( *Met ` X ) -> J e. Top )
81 70 80 syl 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> J e. Top )
82 eqid 
 |-  U. J = U. J
83 82 opncld 
 |-  ( ( J e. Top /\ m e. J ) -> ( U. J \ m ) e. ( Clsd ` J ) )
84 81 52 83 syl2anc 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> ( U. J \ m ) e. ( Clsd ` J ) )
85 79 84 eqeltrd 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> ( X \ m ) e. ( Clsd ` J ) )
86 cldcls 
 |-  ( ( X \ m ) e. ( Clsd ` J ) -> ( ( cls ` J ) ` ( X \ m ) ) = ( X \ m ) )
87 85 86 syl 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> ( ( cls ` J ) ` ( X \ m ) ) = ( X \ m ) )
88 78 87 neleqtrrd 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> -. y e. ( ( cls ` J ) ` ( X \ m ) ) )
89 45 1 metdseq0 
 |-  ( ( D e. ( *Met ` X ) /\ ( X \ m ) C_ X /\ y e. X ) -> ( ( ( w e. X |-> inf ( ran ( z e. ( X \ m ) |-> ( w D z ) ) , RR* , < ) ) ` y ) = 0 <-> y e. ( ( cls ` J ) ` ( X \ m ) ) ) )
90 70 49 44 89 syl3anc 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> ( ( ( w e. X |-> inf ( ran ( z e. ( X \ m ) |-> ( w D z ) ) , RR* , < ) ) ` y ) = 0 <-> y e. ( ( cls ` J ) ` ( X \ m ) ) ) )
91 90 necon3abid 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> ( ( ( w e. X |-> inf ( ran ( z e. ( X \ m ) |-> ( w D z ) ) , RR* , < ) ) ` y ) =/= 0 <-> -. y e. ( ( cls ` J ) ` ( X \ m ) ) ) )
92 88 91 mpbird 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> ( ( w e. X |-> inf ( ran ( z e. ( X \ m ) |-> ( w D z ) ) , RR* , < ) ) ` y ) =/= 0 )
93 67 76 92 ne0gt0d 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> 0 < ( ( w e. X |-> inf ( ran ( z e. ( X \ m ) |-> ( w D z ) ) , RR* , < ) ) ` y ) )
94 93 47 breqtrd 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> 0 < inf ( ran ( z e. ( X \ m ) |-> ( y D z ) ) , RR* , < ) )
95 6 ad2antrr 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> U e. Fin )
96 37 adantlr 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) /\ k e. U ) -> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) e. RR )
97 17 ad2antrr 
 |-  ( ( ( ph /\ y e. X ) /\ k e. U ) -> D e. ( *Met ` X ) )
98 30 metdsf 
 |-  ( ( D e. ( *Met ` X ) /\ ( X \ k ) C_ X ) -> ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) : X --> ( 0 [,] +oo ) )
99 97 11 98 syl2anc 
 |-  ( ( ( ph /\ y e. X ) /\ k e. U ) -> ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) : X --> ( 0 [,] +oo ) )
100 30 fmpt 
 |-  ( A. y e. X inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) e. ( 0 [,] +oo ) <-> ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) : X --> ( 0 [,] +oo ) )
101 99 100 sylibr 
 |-  ( ( ( ph /\ y e. X ) /\ k e. U ) -> A. y e. X inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) e. ( 0 [,] +oo ) )
102 rsp 
 |-  ( A. y e. X inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) e. ( 0 [,] +oo ) -> ( y e. X -> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) e. ( 0 [,] +oo ) ) )
103 101 35 102 sylc 
 |-  ( ( ( ph /\ y e. X ) /\ k e. U ) -> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) e. ( 0 [,] +oo ) )
104 elxrge0 
 |-  ( inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) e. ( 0 [,] +oo ) <-> ( inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) e. RR* /\ 0 <_ inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) )
105 103 104 sylib 
 |-  ( ( ( ph /\ y e. X ) /\ k e. U ) -> ( inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) e. RR* /\ 0 <_ inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) )
106 105 simprd 
 |-  ( ( ( ph /\ y e. X ) /\ k e. U ) -> 0 <_ inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) )
107 106 adantlr 
 |-  ( ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) /\ k e. U ) -> 0 <_ inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) )
108 difeq2 
 |-  ( k = m -> ( X \ k ) = ( X \ m ) )
109 108 mpteq1d 
 |-  ( k = m -> ( z e. ( X \ k ) |-> ( y D z ) ) = ( z e. ( X \ m ) |-> ( y D z ) ) )
110 109 rneqd 
 |-  ( k = m -> ran ( z e. ( X \ k ) |-> ( y D z ) ) = ran ( z e. ( X \ m ) |-> ( y D z ) ) )
111 110 infeq1d 
 |-  ( k = m -> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) = inf ( ran ( z e. ( X \ m ) |-> ( y D z ) ) , RR* , < ) )
112 95 96 107 111 51 fsumge1 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> inf ( ran ( z e. ( X \ m ) |-> ( y D z ) ) , RR* , < ) <_ sum_ k e. U inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) )
113 43 68 69 94 112 ltletrd 
 |-  ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> 0 < sum_ k e. U inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) )
114 42 113 rexlimddv 
 |-  ( ( ph /\ y e. X ) -> 0 < sum_ k e. U inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) )
115 38 114 elrpd 
 |-  ( ( ph /\ y e. X ) -> sum_ k e. U inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) e. RR+ )
116 115 8 fmptd 
 |-  ( ph -> F : X --> RR+ )