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+ )