Metamath Proof Explorer


Theorem sge0f1o

Description: Re-index a nonnegative extended sum using a bijection. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0f1o.1 kφ
sge0f1o.2 nφ
sge0f1o.3 k=GB=D
sge0f1o.4 φCV
sge0f1o.5 φF:C1-1 ontoA
sge0f1o.6 φnCFn=G
sge0f1o.7 φkAB0+∞
Assertion sge0f1o φsum^kAB=sum^nCD

Proof

Step Hyp Ref Expression
1 sge0f1o.1 kφ
2 sge0f1o.2 nφ
3 sge0f1o.3 k=GB=D
4 sge0f1o.4 φCV
5 sge0f1o.5 φF:C1-1 ontoA
6 sge0f1o.6 φnCFn=G
7 sge0f1o.7 φkAB0+∞
8 f1ofo F:C1-1 ontoAF:ContoA
9 5 8 syl φF:ContoA
10 fornex CVF:ContoAAV
11 4 9 10 sylc φAV
12 11 adantr φ+∞rannCDAV
13 eqid kAB=kAB
14 1 7 13 fmptdf φkAB:A0+∞
15 14 adantr φ+∞rannCDkAB:A0+∞
16 pnfex +∞V
17 eqid nCD=nCD
18 17 elrnmpt +∞V+∞rannCDnC+∞=D
19 16 18 ax-mp +∞rannCDnC+∞=D
20 19 biimpi +∞rannCDnC+∞=D
21 20 adantl φ+∞rannCDnC+∞=D
22 nfv n+∞rankAB
23 simp3 φnC+∞=D+∞=D
24 f1of F:C1-1 ontoAF:CA
25 5 24 syl φF:CA
26 25 ffvelrnda φnCFnA
27 nfcv _kFn
28 nfv kFn=G
29 27 nfcsb1 _kFn/kB
30 nfcv _kD
31 29 30 nfeq kFn/kB=D
32 28 31 nfim kFn=GFn/kB=D
33 eqeq1 k=Fnk=GFn=G
34 csbeq1a k=FnB=Fn/kB
35 34 eqeq1d k=FnB=DFn/kB=D
36 33 35 imbi12d k=Fnk=GB=DFn=GFn/kB=D
37 27 32 36 3 vtoclgf FnAFn=GFn/kB=D
38 26 6 37 sylc φnCFn/kB=D
39 38 eqcomd φnCD=Fn/kB
40 39 3adant3 φnC+∞=DD=Fn/kB
41 23 40 eqtrd φnC+∞=D+∞=Fn/kB
42 simpl φnCφ
43 42 26 jca φnCφFnA
44 nfv kFnA
45 1 44 nfan kφFnA
46 29 nfel1 kFn/kB0+∞
47 45 46 nfim kφFnAFn/kB0+∞
48 eleq1 k=FnkAFnA
49 48 anbi2d k=FnφkAφFnA
50 34 eleq1d k=FnB0+∞Fn/kB0+∞
51 49 50 imbi12d k=FnφkAB0+∞φFnAFn/kB0+∞
52 27 47 51 7 vtoclgf FnAφFnAFn/kB0+∞
53 26 43 52 sylc φnCFn/kB0+∞
54 29 13 34 elrnmpt1sf FnAFn/kB0+∞Fn/kBrankAB
55 26 53 54 syl2anc φnCFn/kBrankAB
56 55 3adant3 φnC+∞=DFn/kBrankAB
57 41 56 eqeltrd φnC+∞=D+∞rankAB
58 57 3exp φnC+∞=D+∞rankAB
59 2 22 58 rexlimd φnC+∞=D+∞rankAB
60 59 adantr φ+∞rannCDnC+∞=D+∞rankAB
61 21 60 mpd φ+∞rannCD+∞rankAB
62 12 15 61 sge0pnfval φ+∞rannCDsum^kAB=+∞
63 4 adantr φ+∞rannCDCV
64 39 53 eqeltrd φnCD0+∞
65 2 64 17 fmptdf φnCD:C0+∞
66 65 adantr φ+∞rannCDnCD:C0+∞
67 simpr φ+∞rannCD+∞rannCD
68 63 66 67 sge0pnfval φ+∞rannCDsum^nCD=+∞
69 62 68 eqtr4d φ+∞rannCDsum^kAB=sum^nCD
70 sumex kyBV
71 70 a1i φ¬+∞rannCDy𝒫AFinkyBV
72 cnvimass F-1ydomF
73 72 25 fssdm φF-1yC
74 25 4 fexd φFV
75 cnvexg FVF-1V
76 74 75 syl φF-1V
77 imaexg F-1VF-1yV
78 76 77 syl φF-1yV
79 elpwg F-1yVF-1y𝒫CF-1yC
80 78 79 syl φF-1y𝒫CF-1yC
81 73 80 mpbird φF-1y𝒫C
82 81 adantr φy𝒫AFinF-1y𝒫C
83 f1ocnv F:C1-1 ontoAF-1:A1-1 ontoC
84 5 83 syl φF-1:A1-1 ontoC
85 f1ofun F-1:A1-1 ontoCFunF-1
86 84 85 syl φFunF-1
87 86 adantr φy𝒫AFinFunF-1
88 elinel2 y𝒫AFinyFin
89 88 adantl φy𝒫AFinyFin
90 imafi FunF-1yFinF-1yFin
91 87 89 90 syl2anc φy𝒫AFinF-1yFin
92 82 91 elind φy𝒫AFinF-1y𝒫CFin
93 92 adantlr φ¬+∞rannCDy𝒫AFinF-1y𝒫CFin
94 nfv k¬+∞rannCD
95 1 94 nfan kφ¬+∞rannCD
96 nfv ky𝒫AFin
97 95 96 nfan kφ¬+∞rannCDy𝒫AFin
98 nfcv _n+∞
99 nfmpt1 _nnCD
100 99 nfrn _nrannCD
101 98 100 nfel n+∞rannCD
102 101 nfn n¬+∞rannCD
103 2 102 nfan nφ¬+∞rannCD
104 nfv ny𝒫AFin
105 103 104 nfan nφ¬+∞rannCDy𝒫AFin
106 91 adantlr φ¬+∞rannCDy𝒫AFinF-1yFin
107 f1of1 F:C1-1 ontoAF:C1-1A
108 5 107 syl φF:C1-1A
109 108 adantr φy𝒫AFinF:C1-1A
110 80 adantr φy𝒫AFinF-1y𝒫CF-1yC
111 82 110 mpbid φy𝒫AFinF-1yC
112 f1ores F:C1-1AF-1yCFF-1y:F-1y1-1 ontoFF-1y
113 109 111 112 syl2anc φy𝒫AFinFF-1y:F-1y1-1 ontoFF-1y
114 9 adantr φy𝒫AFinF:ContoA
115 elpwinss y𝒫AFinyA
116 115 adantl φy𝒫AFinyA
117 foimacnv F:ContoAyAFF-1y=y
118 114 116 117 syl2anc φy𝒫AFinFF-1y=y
119 118 f1oeq3d φy𝒫AFinFF-1y:F-1y1-1 ontoFF-1yFF-1y:F-1y1-1 ontoy
120 113 119 mpbid φy𝒫AFinFF-1y:F-1y1-1 ontoy
121 120 adantlr φ¬+∞rannCDy𝒫AFinFF-1y:F-1y1-1 ontoy
122 78 ad2antrr φy𝒫AFinnF-1yF-1yV
123 simpll φy𝒫AFinnF-1yφ
124 92 adantr φy𝒫AFinnF-1yF-1y𝒫CFin
125 simpr φy𝒫AFinnF-1ynF-1y
126 123 124 125 jca31 φy𝒫AFinnF-1yφF-1y𝒫CFinnF-1y
127 eleq1 x=F-1yx𝒫CFinF-1y𝒫CFin
128 127 anbi2d x=F-1yφx𝒫CFinφF-1y𝒫CFin
129 eleq2 x=F-1ynxnF-1y
130 128 129 anbi12d x=F-1yφx𝒫CFinnxφF-1y𝒫CFinnF-1y
131 reseq2 x=F-1yFx=FF-1y
132 131 fveq1d x=F-1yFxn=FF-1yn
133 132 eqeq1d x=F-1yFxn=GFF-1yn=G
134 130 133 imbi12d x=F-1yφx𝒫CFinnxFxn=GφF-1y𝒫CFinnF-1yFF-1yn=G
135 fvres nxFxn=Fn
136 135 adantl φx𝒫CFinnxFxn=Fn
137 simpll φx𝒫CFinnxφ
138 elpwinss x𝒫CFinxC
139 138 adantl φx𝒫CFinxC
140 139 sselda φx𝒫CFinnxnC
141 137 140 6 syl2anc φx𝒫CFinnxFn=G
142 136 141 eqtrd φx𝒫CFinnxFxn=G
143 134 142 vtoclg F-1yVφF-1y𝒫CFinnF-1yFF-1yn=G
144 122 126 143 sylc φy𝒫AFinnF-1yFF-1yn=G
145 144 adantllr φ¬+∞rannCDy𝒫AFinnF-1yFF-1yn=G
146 78 ad3antrrr φ¬+∞rannCDy𝒫AFinkyF-1yV
147 simpll φ¬+∞rannCDy𝒫AFinkyφ¬+∞rannCD
148 81 ad3antrrr φ¬+∞rannCDy𝒫AFinkyF-1y𝒫C
149 106 adantr φ¬+∞rannCDy𝒫AFinkyF-1yFin
150 148 149 elind φ¬+∞rannCDy𝒫AFinkyF-1y𝒫CFin
151 simpr φy𝒫AFinkyky
152 118 eqcomd φy𝒫AFiny=FF-1y
153 152 adantr φy𝒫AFinkyy=FF-1y
154 151 153 eleqtrd φy𝒫AFinkykFF-1y
155 154 adantllr φ¬+∞rannCDy𝒫AFinkykFF-1y
156 147 150 155 jca31 φ¬+∞rannCDy𝒫AFinkyφ¬+∞rannCDF-1y𝒫CFinkFF-1y
157 127 anbi2d x=F-1yφ¬+∞rannCDx𝒫CFinφ¬+∞rannCDF-1y𝒫CFin
158 imaeq2 x=F-1yFx=FF-1y
159 158 eleq2d x=F-1ykFxkFF-1y
160 157 159 anbi12d x=F-1yφ¬+∞rannCDx𝒫CFinkFxφ¬+∞rannCDF-1y𝒫CFinkFF-1y
161 160 imbi1d x=F-1yφ¬+∞rannCDx𝒫CFinkFxBφ¬+∞rannCDF-1y𝒫CFinkFF-1yB
162 rge0ssre 0+∞
163 ax-resscn
164 162 163 sstri 0+∞
165 simplll φ¬+∞rannCDx𝒫CFinkFxφ
166 simpllr φ¬+∞rannCDx𝒫CFinkFx¬+∞rannCD
167 fimass F:CAFxA
168 25 167 syl φFxA
169 168 ad2antrr φx𝒫CFinkFxFxA
170 simpr φx𝒫CFinkFxkFx
171 169 170 sseldd φx𝒫CFinkFxkA
172 171 adantllr φ¬+∞rannCDx𝒫CFinkFxkA
173 foelrni F:ContoAkAnCFn=k
174 9 173 sylan φkAnCFn=k
175 174 adantlr φ¬+∞rannCDkAnCFn=k
176 nfv nkA
177 103 176 nfan nφ¬+∞rannCDkA
178 nfv nB0+∞
179 csbid k/kB=B
180 179 eqcomi B=k/kB
181 180 a1i φnCFn=kB=k/kB
182 id Fn=kFn=k
183 182 eqcomd Fn=kk=Fn
184 183 csbeq1d Fn=kk/kB=Fn/kB
185 184 3ad2ant3 φnCFn=kk/kB=Fn/kB
186 38 idi φnCFn/kB=D
187 186 3adant3 φnCFn=kFn/kB=D
188 181 185 187 3eqtrd φnCFn=kB=D
189 188 3adant1r φ¬+∞rannCDnCFn=kB=D
190 0xr 0*
191 190 a1i φnC¬D0+∞0*
192 pnfxr +∞*
193 192 a1i φnC¬D0+∞+∞*
194 64 adantr φnC¬D0+∞D0+∞
195 simpr φnC¬D0+∞¬D0+∞
196 191 193 194 195 eliccnelico φnC¬D0+∞D=+∞
197 196 eqcomd φnC¬D0+∞+∞=D
198 simpr φnCnC
199 64 idi φnCD0+∞
200 17 elrnmpt1 nCD0+∞DrannCD
201 198 199 200 syl2anc φnCDrannCD
202 201 adantr φnC¬D0+∞DrannCD
203 197 202 eqeltrd φnC¬D0+∞+∞rannCD
204 203 adantllr φ¬+∞rannCDnC¬D0+∞+∞rannCD
205 simpllr φ¬+∞rannCDnC¬D0+∞¬+∞rannCD
206 204 205 condan φ¬+∞rannCDnCD0+∞
207 206 3adant3 φ¬+∞rannCDnCFn=kD0+∞
208 189 207 eqeltrd φ¬+∞rannCDnCFn=kB0+∞
209 208 3exp φ¬+∞rannCDnCFn=kB0+∞
210 209 adantr φ¬+∞rannCDkAnCFn=kB0+∞
211 177 178 210 rexlimd φ¬+∞rannCDkAnCFn=kB0+∞
212 175 211 mpd φ¬+∞rannCDkAB0+∞
213 165 166 172 212 syl21anc φ¬+∞rannCDx𝒫CFinkFxB0+∞
214 164 213 sselid φ¬+∞rannCDx𝒫CFinkFxB
215 214 idi φ¬+∞rannCDx𝒫CFinkFxB
216 161 215 vtoclg F-1yVφ¬+∞rannCDF-1y𝒫CFinkFF-1yB
217 146 156 216 sylc φ¬+∞rannCDy𝒫AFinkyB
218 97 105 3 106 121 145 217 fsumf1of φ¬+∞rannCDy𝒫AFinkyB=nF-1yD
219 sumeq1 x=F-1ynxD=nF-1yD
220 219 rspceeqv F-1y𝒫CFinkyB=nF-1yDx𝒫CFinkyB=nxD
221 93 218 220 syl2anc φ¬+∞rannCDy𝒫AFinx𝒫CFinkyB=nxD
222 71 221 rnmptssrn φ¬+∞rannCDrany𝒫AFinkyBranx𝒫CFinnxD
223 sumex nxDV
224 223 a1i φ¬+∞rannCDx𝒫CFinnxDV
225 11 168 ssexd φFxV
226 elpwg FxVFx𝒫AFxA
227 225 226 syl φFx𝒫AFxA
228 168 227 mpbird φFx𝒫A
229 228 adantr φx𝒫CFinFx𝒫A
230 25 ffund φFunF
231 230 adantr φx𝒫CFinFunF
232 elinel2 x𝒫CFinxFin
233 232 adantl φx𝒫CFinxFin
234 imafi FunFxFinFxFin
235 231 233 234 syl2anc φx𝒫CFinFxFin
236 229 235 elind φx𝒫CFinFx𝒫AFin
237 236 adantlr φ¬+∞rannCDx𝒫CFinFx𝒫AFin
238 nfv kx𝒫CFin
239 95 238 nfan kφ¬+∞rannCDx𝒫CFin
240 nfv nx𝒫CFin
241 103 240 nfan nφ¬+∞rannCDx𝒫CFin
242 232 adantl φ¬+∞rannCDx𝒫CFinxFin
243 108 adantr φx𝒫CFinF:C1-1A
244 f1ores F:C1-1AxCFx:x1-1 ontoFx
245 243 139 244 syl2anc φx𝒫CFinFx:x1-1 ontoFx
246 245 adantlr φ¬+∞rannCDx𝒫CFinFx:x1-1 ontoFx
247 142 adantllr φ¬+∞rannCDx𝒫CFinnxFxn=G
248 239 241 3 242 246 247 214 fsumf1of φ¬+∞rannCDx𝒫CFinkFxB=nxD
249 248 eqcomd φ¬+∞rannCDx𝒫CFinnxD=kFxB
250 sumeq1 y=FxkyB=kFxB
251 250 rspceeqv Fx𝒫AFinnxD=kFxBy𝒫AFinnxD=kyB
252 237 249 251 syl2anc φ¬+∞rannCDx𝒫CFiny𝒫AFinnxD=kyB
253 224 252 rnmptssrn φ¬+∞rannCDranx𝒫CFinnxDrany𝒫AFinkyB
254 222 253 eqssd φ¬+∞rannCDrany𝒫AFinkyB=ranx𝒫CFinnxD
255 254 supeq1d φ¬+∞rannCDsuprany𝒫AFinkyB*<=supranx𝒫CFinnxD*<
256 11 adantr φ¬+∞rannCDAV
257 95 256 212 sge0revalmpt φ¬+∞rannCDsum^kAB=suprany𝒫AFinkyB*<
258 4 adantr φ¬+∞rannCDCV
259 103 258 206 sge0revalmpt φ¬+∞rannCDsum^nCD=supranx𝒫CFinnxD*<
260 255 257 259 3eqtr4d φ¬+∞rannCDsum^kAB=sum^nCD
261 69 260 pm2.61dan φsum^kAB=sum^nCD