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=MetOpenD
lebnum.d φDMetX
lebnum.c φJComp
lebnum.s φUJ
lebnum.u φX=U
lebnumlem1.u φUFin
lebnumlem1.n φ¬XU
lebnumlem1.f F=yXkUsupranzXkyDz*<
Assertion lebnumlem1 φF:X+

Proof

Step Hyp Ref Expression
1 lebnum.j J=MetOpenD
2 lebnum.d φDMetX
3 lebnum.c φJComp
4 lebnum.s φUJ
5 lebnum.u φX=U
6 lebnumlem1.u φUFin
7 lebnumlem1.n φ¬XU
8 lebnumlem1.f F=yXkUsupranzXkyDz*<
9 6 adantr φyXUFin
10 2 ad2antrr φyXkUDMetX
11 difssd φyXkUXkX
12 4 adantr φyXUJ
13 12 sselda φyXkUkJ
14 elssuni kJkJ
15 13 14 syl φyXkUkJ
16 metxmet DMetXD∞MetX
17 2 16 syl φD∞MetX
18 1 mopnuni D∞MetXX=J
19 17 18 syl φX=J
20 19 ad2antrr φyXkUX=J
21 15 20 sseqtrrd φyXkUkX
22 eleq1 k=XkUXU
23 22 notbid k=X¬kU¬XU
24 7 23 syl5ibrcom φk=X¬kU
25 24 necon2ad φkUkX
26 25 adantr φyXkUkX
27 26 imp φyXkUkX
28 pssdifn0 kXkXXk
29 21 27 28 syl2anc φyXkUXk
30 eqid yXsupranzXkyDz*<=yXsupranzXkyDz*<
31 30 metdsre DMetXXkXXkyXsupranzXkyDz*<:X
32 10 11 29 31 syl3anc φyXkUyXsupranzXkyDz*<:X
33 30 fmpt yXsupranzXkyDz*<yXsupranzXkyDz*<:X
34 32 33 sylibr φyXkUyXsupranzXkyDz*<
35 simplr φyXkUyX
36 rsp yXsupranzXkyDz*<yXsupranzXkyDz*<
37 34 35 36 sylc φyXkUsupranzXkyDz*<
38 9 37 fsumrecl φyXkUsupranzXkyDz*<
39 5 eleq2d φyXyU
40 39 biimpa φyXyU
41 eluni2 yUmUym
42 40 41 sylib φyXmUym
43 0red φyXmUym0
44 simplr φyXmUymyX
45 eqid wXsupranzXmwDz*<=wXsupranzXmwDz*<
46 45 metdsval yXwXsupranzXmwDz*<y=supranzXmyDz*<
47 44 46 syl φyXmUymwXsupranzXmwDz*<y=supranzXmyDz*<
48 2 ad2antrr φyXmUymDMetX
49 difssd φyXmUymXmX
50 4 ad2antrr φyXmUymUJ
51 simprl φyXmUymmU
52 50 51 sseldd φyXmUymmJ
53 elssuni mJmJ
54 52 53 syl φyXmUymmJ
55 48 16 18 3syl φyXmUymX=J
56 54 55 sseqtrrd φyXmUymmX
57 eleq1 m=XmUXU
58 57 notbid m=X¬mU¬XU
59 7 58 syl5ibrcom φm=X¬mU
60 59 necon2ad φmUmX
61 60 ad2antrr φyXmUymmUmX
62 51 61 mpd φyXmUymmX
63 pssdifn0 mXmXXm
64 56 62 63 syl2anc φyXmUymXm
65 45 metdsre DMetXXmXXmwXsupranzXmwDz*<:X
66 48 49 64 65 syl3anc φyXmUymwXsupranzXmwDz*<:X
67 66 44 ffvelrnd φyXmUymwXsupranzXmwDz*<y
68 47 67 eqeltrrd φyXmUymsupranzXmyDz*<
69 38 adantr φyXmUymkUsupranzXkyDz*<
70 17 ad2antrr φyXmUymD∞MetX
71 45 metdsf D∞MetXXmXwXsupranzXmwDz*<:X0+∞
72 70 49 71 syl2anc φyXmUymwXsupranzXmwDz*<:X0+∞
73 72 44 ffvelrnd φyXmUymwXsupranzXmwDz*<y0+∞
74 elxrge0 wXsupranzXmwDz*<y0+∞wXsupranzXmwDz*<y*0wXsupranzXmwDz*<y
75 73 74 sylib φyXmUymwXsupranzXmwDz*<y*0wXsupranzXmwDz*<y
76 75 simprd φyXmUym0wXsupranzXmwDz*<y
77 elndif ym¬yXm
78 77 ad2antll φyXmUym¬yXm
79 55 difeq1d φyXmUymXm=Jm
80 1 mopntop D∞MetXJTop
81 70 80 syl φyXmUymJTop
82 eqid J=J
83 82 opncld JTopmJJmClsdJ
84 81 52 83 syl2anc φyXmUymJmClsdJ
85 79 84 eqeltrd φyXmUymXmClsdJ
86 cldcls XmClsdJclsJXm=Xm
87 85 86 syl φyXmUymclsJXm=Xm
88 78 87 neleqtrrd φyXmUym¬yclsJXm
89 45 1 metdseq0 D∞MetXXmXyXwXsupranzXmwDz*<y=0yclsJXm
90 70 49 44 89 syl3anc φyXmUymwXsupranzXmwDz*<y=0yclsJXm
91 90 necon3abid φyXmUymwXsupranzXmwDz*<y0¬yclsJXm
92 88 91 mpbird φyXmUymwXsupranzXmwDz*<y0
93 67 76 92 ne0gt0d φyXmUym0<wXsupranzXmwDz*<y
94 93 47 breqtrd φyXmUym0<supranzXmyDz*<
95 6 ad2antrr φyXmUymUFin
96 37 adantlr φyXmUymkUsupranzXkyDz*<
97 17 ad2antrr φyXkUD∞MetX
98 30 metdsf D∞MetXXkXyXsupranzXkyDz*<:X0+∞
99 97 11 98 syl2anc φyXkUyXsupranzXkyDz*<:X0+∞
100 30 fmpt yXsupranzXkyDz*<0+∞yXsupranzXkyDz*<:X0+∞
101 99 100 sylibr φyXkUyXsupranzXkyDz*<0+∞
102 rsp yXsupranzXkyDz*<0+∞yXsupranzXkyDz*<0+∞
103 101 35 102 sylc φyXkUsupranzXkyDz*<0+∞
104 elxrge0 supranzXkyDz*<0+∞supranzXkyDz*<*0supranzXkyDz*<
105 103 104 sylib φyXkUsupranzXkyDz*<*0supranzXkyDz*<
106 105 simprd φyXkU0supranzXkyDz*<
107 106 adantlr φyXmUymkU0supranzXkyDz*<
108 difeq2 k=mXk=Xm
109 108 mpteq1d k=mzXkyDz=zXmyDz
110 109 rneqd k=mranzXkyDz=ranzXmyDz
111 110 infeq1d k=msupranzXkyDz*<=supranzXmyDz*<
112 95 96 107 111 51 fsumge1 φyXmUymsupranzXmyDz*<kUsupranzXkyDz*<
113 43 68 69 94 112 ltletrd φyXmUym0<kUsupranzXkyDz*<
114 42 113 rexlimddv φyX0<kUsupranzXkyDz*<
115 38 114 elrpd φyXkUsupranzXkyDz*<+
116 115 8 fmptd φF:X+