Metamath Proof Explorer


Theorem imasdsf1olem

Description: Lemma for imasdsf1o . (Contributed by Mario Carneiro, 21-Aug-2015) (Proof shortened by AV, 6-Oct-2020)

Ref Expression
Hypotheses imasdsf1o.u φU=F𝑠R
imasdsf1o.v φV=BaseR
imasdsf1o.f φF:V1-1 ontoB
imasdsf1o.r φRZ
imasdsf1o.e E=distRV×V
imasdsf1o.d D=distU
imasdsf1o.m φE∞MetV
imasdsf1o.x φXV
imasdsf1o.y φYV
imasdsf1o.w W=𝑠*𝑠*−∞
imasdsf1o.s S=hV×V1n|F1sth1=FXF2ndhn=FYi1n1F2ndhi=F1sthi+1
imasdsf1o.t T=nrangS𝑠*Eg
Assertion imasdsf1olem φFXDFY=XEY

Proof

Step Hyp Ref Expression
1 imasdsf1o.u φU=F𝑠R
2 imasdsf1o.v φV=BaseR
3 imasdsf1o.f φF:V1-1 ontoB
4 imasdsf1o.r φRZ
5 imasdsf1o.e E=distRV×V
6 imasdsf1o.d D=distU
7 imasdsf1o.m φE∞MetV
8 imasdsf1o.x φXV
9 imasdsf1o.y φYV
10 imasdsf1o.w W=𝑠*𝑠*−∞
11 imasdsf1o.s S=hV×V1n|F1sth1=FXF2ndhn=FYi1n1F2ndhi=F1sthi+1
12 imasdsf1o.t T=nrangS𝑠*Eg
13 f1ofo F:V1-1 ontoBF:VontoB
14 3 13 syl φF:VontoB
15 eqid distR=distR
16 f1of F:V1-1 ontoBF:VB
17 3 16 syl φF:VB
18 17 8 ffvelrnd φFXB
19 17 9 ffvelrnd φFYB
20 1 2 14 4 15 6 18 19 11 5 imasdsval2 φFXDFY=supnrangS𝑠*Eg*<
21 12 infeq1i supT*<=supnrangS𝑠*Eg*<
22 20 21 eqtr4di φFXDFY=supT*<
23 xrsbas *=Base𝑠*
24 xrsadd +𝑒=+𝑠*
25 xrsex 𝑠*V
26 25 a1i φngS𝑠*V
27 fzfid φngS1nFin
28 difss *−∞*
29 28 a1i φngS*−∞*
30 xmetf E∞MetVE:V×V*
31 ffn E:V×V*EFnV×V
32 7 30 31 3syl φEFnV×V
33 xmetcl E∞MetVfVgVfEg*
34 xmetge0 E∞MetVfVgV0fEg
35 ge0nemnf fEg*0fEgfEg−∞
36 33 34 35 syl2anc E∞MetVfVgVfEg−∞
37 eldifsn fEg*−∞fEg*fEg−∞
38 33 36 37 sylanbrc E∞MetVfVgVfEg*−∞
39 38 3expb E∞MetVfVgVfEg*−∞
40 7 39 sylan φfVgVfEg*−∞
41 40 ralrimivva φfVgVfEg*−∞
42 ffnov E:V×V*−∞EFnV×VfVgVfEg*−∞
43 32 41 42 sylanbrc φE:V×V*−∞
44 43 ad2antrr φngSE:V×V*−∞
45 11 ssrab3 SV×V1n
46 45 a1i φnSV×V1n
47 46 sselda φngSgV×V1n
48 elmapi gV×V1ng:1nV×V
49 47 48 syl φngSg:1nV×V
50 fco E:V×V*−∞g:1nV×VEg:1n*−∞
51 44 49 50 syl2anc φngSEg:1n*−∞
52 0re 0
53 rexr 00*
54 renemnf 00−∞
55 eldifsn 0*−∞0*0−∞
56 53 54 55 sylanbrc 00*−∞
57 52 56 mp1i φngS0*−∞
58 xaddid2 x*0+𝑒x=x
59 xaddid1 x*x+𝑒0=x
60 58 59 jca x*0+𝑒x=xx+𝑒0=x
61 60 adantl φngSx*0+𝑒x=xx+𝑒0=x
62 23 24 10 26 27 29 51 57 61 gsumress φngS𝑠*Eg=WEg
63 10 23 ressbas2 *−∞**−∞=BaseW
64 28 63 ax-mp *−∞=BaseW
65 10 xrs10 0=0W
66 10 xrs1cmn WCMnd
67 66 a1i φngSWCMnd
68 c0ex 0V
69 68 a1i φngS0V
70 51 27 69 fdmfifsupp φngSfinSupp0Eg
71 64 65 67 27 51 70 gsumcl φngSWEg*−∞
72 62 71 eqeltrd φngS𝑠*Eg*−∞
73 72 eldifad φngS𝑠*Eg*
74 73 fmpttd φngS𝑠*Eg:S*
75 74 frnd φnrangS𝑠*Eg*
76 75 ralrimiva φnrangS𝑠*Eg*
77 iunss nrangS𝑠*Eg*nrangS𝑠*Eg*
78 76 77 sylibr φnrangS𝑠*Eg*
79 12 78 eqsstrid φT*
80 infxrcl T*supT*<*
81 79 80 syl φsupT*<*
82 xmetcl E∞MetVXVYVXEY*
83 7 8 9 82 syl3anc φXEY*
84 1nn 1
85 1ex 1V
86 opex XYV
87 85 86 f1osn 1XY:11-1 ontoXY
88 f1of 1XY:11-1 ontoXY1XY:1XY
89 87 88 ax-mp 1XY:1XY
90 8 9 opelxpd φXYV×V
91 90 snssd φXYV×V
92 fss 1XY:1XYXYV×V1XY:1V×V
93 89 91 92 sylancr φ1XY:1V×V
94 7 elfvexd φVV
95 94 94 xpexd φV×VV
96 snex 1V
97 elmapg V×VV1V1XYV×V11XY:1V×V
98 95 96 97 sylancl φ1XYV×V11XY:1V×V
99 93 98 mpbird φ1XYV×V1
100 op1stg XVYV1stXY=X
101 8 9 100 syl2anc φ1stXY=X
102 101 fveq2d φF1stXY=FX
103 op2ndg XVYV2ndXY=Y
104 8 9 103 syl2anc φ2ndXY=Y
105 104 fveq2d φF2ndXY=FY
106 102 105 jca φF1stXY=FXF2ndXY=FY
107 25 a1i φ𝑠*V
108 snfi 1Fin
109 108 a1i φ1Fin
110 28 a1i φ*−∞*
111 xmetge0 E∞MetVXVYV0XEY
112 7 8 9 111 syl3anc φ0XEY
113 ge0nemnf XEY*0XEYXEY−∞
114 83 112 113 syl2anc φXEY−∞
115 eldifsn XEY*−∞XEY*XEY−∞
116 83 114 115 sylanbrc φXEY*−∞
117 fconst6g XEY*−∞1×XEY:1*−∞
118 116 117 syl φ1×XEY:1*−∞
119 fcoconst EFnV×VXYV×VE1×XY=1×EXY
120 32 90 119 syl2anc φE1×XY=1×EXY
121 85 86 xpsn 1×XY=1XY
122 121 coeq2i E1×XY=E1XY
123 df-ov XEY=EXY
124 123 eqcomi EXY=XEY
125 124 sneqi EXY=XEY
126 125 xpeq2i 1×EXY=1×XEY
127 120 122 126 3eqtr3g φE1XY=1×XEY
128 127 feq1d φE1XY:1*−∞1×XEY:1*−∞
129 118 128 mpbird φE1XY:1*−∞
130 52 56 mp1i φ0*−∞
131 60 adantl φx*0+𝑒x=xx+𝑒0=x
132 23 24 10 107 109 110 129 130 131 gsumress φ𝑠*E1XY=WE1XY
133 fconstmpt 1×XEY=j1XEY
134 127 133 eqtrdi φE1XY=j1XEY
135 134 oveq2d φWE1XY=Wj1XEY
136 cmnmnd WCMndWMnd
137 66 136 mp1i φWMnd
138 84 a1i φ1
139 eqidd j=1XEY=XEY
140 64 139 gsumsn WMnd1XEY*−∞Wj1XEY=XEY
141 137 138 116 140 syl3anc φWj1XEY=XEY
142 132 135 141 3eqtrrd φXEY=𝑠*E1XY
143 fveq1 g=1XYg1=1XY1
144 85 86 fvsn 1XY1=XY
145 143 144 eqtrdi g=1XYg1=XY
146 145 fveq2d g=1XY1stg1=1stXY
147 146 fveqeq2d g=1XYF1stg1=FXF1stXY=FX
148 145 fveq2d g=1XY2ndg1=2ndXY
149 148 fveqeq2d g=1XYF2ndg1=FYF2ndXY=FY
150 147 149 anbi12d g=1XYF1stg1=FXF2ndg1=FYF1stXY=FXF2ndXY=FY
151 coeq2 g=1XYEg=E1XY
152 151 oveq2d g=1XY𝑠*Eg=𝑠*E1XY
153 152 eqeq2d g=1XYXEY=𝑠*EgXEY=𝑠*E1XY
154 150 153 anbi12d g=1XYF1stg1=FXF2ndg1=FYXEY=𝑠*EgF1stXY=FXF2ndXY=FYXEY=𝑠*E1XY
155 154 rspcev 1XYV×V1F1stXY=FXF2ndXY=FYXEY=𝑠*E1XYgV×V1F1stg1=FXF2ndg1=FYXEY=𝑠*Eg
156 99 106 142 155 syl12anc φgV×V1F1stg1=FXF2ndg1=FYXEY=𝑠*Eg
157 ovex XEYV
158 eqid gS𝑠*Eg=gS𝑠*Eg
159 158 elrnmpt XEYVXEYrangS𝑠*EggSXEY=𝑠*Eg
160 157 159 ax-mp XEYrangS𝑠*EggSXEY=𝑠*Eg
161 11 rexeqi gSXEY=𝑠*EgghV×V1n|F1sth1=FXF2ndhn=FYi1n1F2ndhi=F1sthi+1XEY=𝑠*Eg
162 fveq1 h=gh1=g1
163 162 fveq2d h=g1sth1=1stg1
164 163 fveqeq2d h=gF1sth1=FXF1stg1=FX
165 fveq1 h=ghn=gn
166 165 fveq2d h=g2ndhn=2ndgn
167 166 fveqeq2d h=gF2ndhn=FYF2ndgn=FY
168 fveq1 h=ghi=gi
169 168 fveq2d h=g2ndhi=2ndgi
170 169 fveq2d h=gF2ndhi=F2ndgi
171 fveq1 h=ghi+1=gi+1
172 171 fveq2d h=g1sthi+1=1stgi+1
173 172 fveq2d h=gF1sthi+1=F1stgi+1
174 170 173 eqeq12d h=gF2ndhi=F1sthi+1F2ndgi=F1stgi+1
175 174 ralbidv h=gi1n1F2ndhi=F1sthi+1i1n1F2ndgi=F1stgi+1
176 164 167 175 3anbi123d h=gF1sth1=FXF2ndhn=FYi1n1F2ndhi=F1sthi+1F1stg1=FXF2ndgn=FYi1n1F2ndgi=F1stgi+1
177 176 rexrab ghV×V1n|F1sth1=FXF2ndhn=FYi1n1F2ndhi=F1sthi+1XEY=𝑠*EggV×V1nF1stg1=FXF2ndgn=FYi1n1F2ndgi=F1stgi+1XEY=𝑠*Eg
178 161 177 bitri gSXEY=𝑠*EggV×V1nF1stg1=FXF2ndgn=FYi1n1F2ndgi=F1stgi+1XEY=𝑠*Eg
179 oveq2 n=11n=11
180 1z 1
181 fzsn 111=1
182 180 181 ax-mp 11=1
183 179 182 eqtrdi n=11n=1
184 183 oveq2d n=1V×V1n=V×V1
185 df-3an F1stg1=FXF2ndgn=FYi1n1F2ndgi=F1stgi+1F1stg1=FXF2ndgn=FYi1n1F2ndgi=F1stgi+1
186 ral0 iF2ndgi=F1stgi+1
187 oveq1 n=1n1=11
188 1m1e0 11=0
189 187 188 eqtrdi n=1n1=0
190 189 oveq2d n=11n1=10
191 fz10 10=
192 190 191 eqtrdi n=11n1=
193 192 raleqdv n=1i1n1F2ndgi=F1stgi+1iF2ndgi=F1stgi+1
194 186 193 mpbiri n=1i1n1F2ndgi=F1stgi+1
195 194 biantrud n=1F1stg1=FXF2ndgn=FYF1stg1=FXF2ndgn=FYi1n1F2ndgi=F1stgi+1
196 2fveq3 n=12ndgn=2ndg1
197 196 fveqeq2d n=1F2ndgn=FYF2ndg1=FY
198 197 anbi2d n=1F1stg1=FXF2ndgn=FYF1stg1=FXF2ndg1=FY
199 195 198 bitr3d n=1F1stg1=FXF2ndgn=FYi1n1F2ndgi=F1stgi+1F1stg1=FXF2ndg1=FY
200 185 199 syl5bb n=1F1stg1=FXF2ndgn=FYi1n1F2ndgi=F1stgi+1F1stg1=FXF2ndg1=FY
201 200 anbi1d n=1F1stg1=FXF2ndgn=FYi1n1F2ndgi=F1stgi+1XEY=𝑠*EgF1stg1=FXF2ndg1=FYXEY=𝑠*Eg
202 184 201 rexeqbidv n=1gV×V1nF1stg1=FXF2ndgn=FYi1n1F2ndgi=F1stgi+1XEY=𝑠*EggV×V1F1stg1=FXF2ndg1=FYXEY=𝑠*Eg
203 178 202 syl5bb n=1gSXEY=𝑠*EggV×V1F1stg1=FXF2ndg1=FYXEY=𝑠*Eg
204 160 203 syl5bb n=1XEYrangS𝑠*EggV×V1F1stg1=FXF2ndg1=FYXEY=𝑠*Eg
205 204 rspcev 1gV×V1F1stg1=FXF2ndg1=FYXEY=𝑠*EgnXEYrangS𝑠*Eg
206 84 156 205 sylancr φnXEYrangS𝑠*Eg
207 eliun XEYnrangS𝑠*EgnXEYrangS𝑠*Eg
208 206 207 sylibr φXEYnrangS𝑠*Eg
209 208 12 eleqtrrdi φXEYT
210 infxrlb T*XEYTsupT*<XEY
211 79 209 210 syl2anc φsupT*<XEY
212 12 eleq2i pTpnrangS𝑠*Eg
213 eliun pnrangS𝑠*EgnprangS𝑠*Eg
214 212 213 bitri pTnprangS𝑠*Eg
215 158 elrnmpt pVprangS𝑠*EggSp=𝑠*Eg
216 215 elv prangS𝑠*EggSp=𝑠*Eg
217 176 11 elrab2 gSgV×V1nF1stg1=FXF2ndgn=FYi1n1F2ndgi=F1stgi+1
218 217 simprbi gSF1stg1=FXF2ndgn=FYi1n1F2ndgi=F1stgi+1
219 218 adantl φngSF1stg1=FXF2ndgn=FYi1n1F2ndgi=F1stgi+1
220 219 simp2d φngSF2ndgn=FY
221 3 ad2antrr φngSF:V1-1 ontoB
222 f1of1 F:V1-1 ontoBF:V1-1B
223 221 222 syl φngSF:V1-1B
224 simplr φngSn
225 elfz1end nn1n
226 224 225 sylib φngSn1n
227 49 226 ffvelrnd φngSgnV×V
228 xp2nd gnV×V2ndgnV
229 227 228 syl φngS2ndgnV
230 9 ad2antrr φngSYV
231 f1fveq F:V1-1B2ndgnVYVF2ndgn=FY2ndgn=Y
232 223 229 230 231 syl12anc φngSF2ndgn=FY2ndgn=Y
233 220 232 mpbid φngS2ndgn=Y
234 233 oveq2d φngSXE2ndgn=XEY
235 eleq1 m=1m1n11n
236 2fveq3 m=12ndgm=2ndg1
237 236 oveq2d m=1XE2ndgm=XE2ndg1
238 oveq2 m=11m=11
239 238 182 eqtrdi m=11m=1
240 239 reseq2d m=1Eg1m=Eg1
241 240 oveq2d m=1WEg1m=WEg1
242 237 241 breq12d m=1XE2ndgmWEg1mXE2ndg1WEg1
243 235 242 imbi12d m=1m1nXE2ndgmWEg1m11nXE2ndg1WEg1
244 243 imbi2d m=1φngSm1nXE2ndgmWEg1mφngS11nXE2ndg1WEg1
245 eleq1 m=xm1nx1n
246 2fveq3 m=x2ndgm=2ndgx
247 246 oveq2d m=xXE2ndgm=XE2ndgx
248 oveq2 m=x1m=1x
249 248 reseq2d m=xEg1m=Eg1x
250 249 oveq2d m=xWEg1m=WEg1x
251 247 250 breq12d m=xXE2ndgmWEg1mXE2ndgxWEg1x
252 245 251 imbi12d m=xm1nXE2ndgmWEg1mx1nXE2ndgxWEg1x
253 252 imbi2d m=xφngSm1nXE2ndgmWEg1mφngSx1nXE2ndgxWEg1x
254 eleq1 m=x+1m1nx+11n
255 2fveq3 m=x+12ndgm=2ndgx+1
256 255 oveq2d m=x+1XE2ndgm=XE2ndgx+1
257 oveq2 m=x+11m=1x+1
258 257 reseq2d m=x+1Eg1m=Eg1x+1
259 258 oveq2d m=x+1WEg1m=WEg1x+1
260 256 259 breq12d m=x+1XE2ndgmWEg1mXE2ndgx+1WEg1x+1
261 254 260 imbi12d m=x+1m1nXE2ndgmWEg1mx+11nXE2ndgx+1WEg1x+1
262 261 imbi2d m=x+1φngSm1nXE2ndgmWEg1mφngSx+11nXE2ndgx+1WEg1x+1
263 eleq1 m=nm1nn1n
264 2fveq3 m=n2ndgm=2ndgn
265 264 oveq2d m=nXE2ndgm=XE2ndgn
266 oveq2 m=n1m=1n
267 266 reseq2d m=nEg1m=Eg1n
268 267 oveq2d m=nWEg1m=WEg1n
269 265 268 breq12d m=nXE2ndgmWEg1mXE2ndgnWEg1n
270 263 269 imbi12d m=nm1nXE2ndgmWEg1mn1nXE2ndgnWEg1n
271 270 imbi2d m=nφngSm1nXE2ndgmWEg1mφngSn1nXE2ndgnWEg1n
272 7 ad2antrr φngSE∞MetV
273 8 ad2antrr φngSXV
274 nnuz =1
275 224 274 eleqtrdi φngSn1
276 eluzfz1 n111n
277 275 276 syl φngS11n
278 49 277 ffvelrnd φngSg1V×V
279 xp2nd g1V×V2ndg1V
280 278 279 syl φngS2ndg1V
281 xmetcl E∞MetVXV2ndg1VXE2ndg1*
282 272 273 280 281 syl3anc φngSXE2ndg1*
283 282 xrleidd φngSXE2ndg1XE2ndg1
284 137 ad2antrr φngSWMnd
285 84 a1i φngS1
286 44 278 ffvelrnd φngSEg1*−∞
287 2fveq3 j=1Egj=Eg1
288 64 287 gsumsn WMnd1Eg1*−∞Wj1Egj=Eg1
289 284 285 286 288 syl3anc φngSWj1Egj=Eg1
290 272 30 syl φngSE:V×V*
291 fcompt E:V×V*g:1nV×VEg=j1nEgj
292 290 49 291 syl2anc φngSEg=j1nEgj
293 292 reseq1d φngSEg1=j1nEgj1
294 277 snssd φngS11n
295 294 resmptd φngSj1nEgj1=j1Egj
296 293 295 eqtrd φngSEg1=j1Egj
297 296 oveq2d φngSWEg1=Wj1Egj
298 df-ov XE2ndg1=EX2ndg1
299 1st2nd2 g1V×Vg1=1stg12ndg1
300 278 299 syl φngSg1=1stg12ndg1
301 219 simp1d φngSF1stg1=FX
302 xp1st g1V×V1stg1V
303 278 302 syl φngS1stg1V
304 f1fveq F:V1-1B1stg1VXVF1stg1=FX1stg1=X
305 223 303 273 304 syl12anc φngSF1stg1=FX1stg1=X
306 301 305 mpbid φngS1stg1=X
307 306 opeq1d φngS1stg12ndg1=X2ndg1
308 300 307 eqtr2d φngSX2ndg1=g1
309 308 fveq2d φngSEX2ndg1=Eg1
310 298 309 eqtrid φngSXE2ndg1=Eg1
311 289 297 310 3eqtr4d φngSWEg1=XE2ndg1
312 283 311 breqtrrd φngSXE2ndg1WEg1
313 312 a1d φngS11nXE2ndg1WEg1
314 simprl φngSxx+11nx
315 314 274 eleqtrdi φngSxx+11nx1
316 simprr φngSxx+11nx+11n
317 peano2fzr x1x+11nx1n
318 315 316 317 syl2anc φngSxx+11nx1n
319 318 expr φngSxx+11nx1n
320 319 imim1d φngSxx1nXE2ndgxWEg1xx+11nXE2ndgxWEg1x
321 272 adantr φngSxx+11nE∞MetV
322 273 adantr φngSxx+11nXV
323 49 adantr φngSxx+11ng:1nV×V
324 323 318 ffvelrnd φngSxx+11ngxV×V
325 xp2nd gxV×V2ndgxV
326 324 325 syl φngSxx+11n2ndgxV
327 xmetcl E∞MetVXV2ndgxVXE2ndgx*
328 321 322 326 327 syl3anc φngSxx+11nXE2ndgx*
329 66 a1i φngSxx+11nWCMnd
330 fzfid φngSxx+11n1xFin
331 51 adantr φngSxx+11nEg:1n*−∞
332 fzsuc x11x+1=1xx+1
333 315 332 syl φngSxx+11n1x+1=1xx+1
334 elfzuz3 x+11nnx+1
335 334 ad2antll φngSxx+11nnx+1
336 fzss2 nx+11x+11n
337 335 336 syl φngSxx+11n1x+11n
338 333 337 eqsstrrd φngSxx+11n1xx+11n
339 338 unssad φngSxx+11n1x1n
340 331 339 fssresd φngSxx+11nEg1x:1x*−∞
341 68 a1i φngSxx+11n0V
342 340 330 341 fdmfifsupp φngSxx+11nfinSupp0Eg1x
343 64 65 329 330 340 342 gsumcl φngSxx+11nWEg1x*−∞
344 343 eldifad φngSxx+11nWEg1x*
345 321 30 syl φngSxx+11nE:V×V*
346 323 316 ffvelrnd φngSxx+11ngx+1V×V
347 345 346 ffvelrnd φngSxx+11nEgx+1*
348 xleadd1a XE2ndgx*WEg1x*Egx+1*XE2ndgxWEg1xXE2ndgx+𝑒Egx+1WEg1x+𝑒Egx+1
349 348 ex XE2ndgx*WEg1x*Egx+1*XE2ndgxWEg1xXE2ndgx+𝑒Egx+1WEg1x+𝑒Egx+1
350 328 344 347 349 syl3anc φngSxx+11nXE2ndgxWEg1xXE2ndgx+𝑒Egx+1WEg1x+𝑒Egx+1
351 xp2nd gx+1V×V2ndgx+1V
352 346 351 syl φngSxx+11n2ndgx+1V
353 xmettri E∞MetVXV2ndgx+1V2ndgxVXE2ndgx+1XE2ndgx+𝑒2ndgxE2ndgx+1
354 321 322 352 326 353 syl13anc φngSxx+11nXE2ndgx+1XE2ndgx+𝑒2ndgxE2ndgx+1
355 1st2nd2 gx+1V×Vgx+1=1stgx+12ndgx+1
356 346 355 syl φngSxx+11ngx+1=1stgx+12ndgx+1
357 2fveq3 i=x2ndgi=2ndgx
358 357 fveq2d i=xF2ndgi=F2ndgx
359 fvoveq1 i=xgi+1=gx+1
360 359 fveq2d i=x1stgi+1=1stgx+1
361 360 fveq2d i=xF1stgi+1=F1stgx+1
362 358 361 eqeq12d i=xF2ndgi=F1stgi+1F2ndgx=F1stgx+1
363 219 simp3d φngSi1n1F2ndgi=F1stgi+1
364 363 adantr φngSxx+11ni1n1F2ndgi=F1stgi+1
365 nnz xx
366 365 ad2antrl φngSxx+11nx
367 eluzp1m1 xnx+1n1x
368 366 335 367 syl2anc φngSxx+11nn1x
369 elfzuzb x1n1x1n1x
370 315 368 369 sylanbrc φngSxx+11nx1n1
371 362 364 370 rspcdva φngSxx+11nF2ndgx=F1stgx+1
372 223 adantr φngSxx+11nF:V1-1B
373 xp1st gx+1V×V1stgx+1V
374 346 373 syl φngSxx+11n1stgx+1V
375 f1fveq F:V1-1B2ndgxV1stgx+1VF2ndgx=F1stgx+12ndgx=1stgx+1
376 372 326 374 375 syl12anc φngSxx+11nF2ndgx=F1stgx+12ndgx=1stgx+1
377 371 376 mpbid φngSxx+11n2ndgx=1stgx+1
378 377 opeq1d φngSxx+11n2ndgx2ndgx+1=1stgx+12ndgx+1
379 356 378 eqtr4d φngSxx+11ngx+1=2ndgx2ndgx+1
380 379 fveq2d φngSxx+11nEgx+1=E2ndgx2ndgx+1
381 df-ov 2ndgxE2ndgx+1=E2ndgx2ndgx+1
382 380 381 eqtr4di φngSxx+11nEgx+1=2ndgxE2ndgx+1
383 382 oveq2d φngSxx+11nXE2ndgx+𝑒Egx+1=XE2ndgx+𝑒2ndgxE2ndgx+1
384 354 383 breqtrrd φngSxx+11nXE2ndgx+1XE2ndgx+𝑒Egx+1
385 xmetcl E∞MetVXV2ndgx+1VXE2ndgx+1*
386 321 322 352 385 syl3anc φngSxx+11nXE2ndgx+1*
387 328 347 xaddcld φngSxx+11nXE2ndgx+𝑒Egx+1*
388 344 347 xaddcld φngSxx+11nWEg1x+𝑒Egx+1*
389 xrletr XE2ndgx+1*XE2ndgx+𝑒Egx+1*WEg1x+𝑒Egx+1*XE2ndgx+1XE2ndgx+𝑒Egx+1XE2ndgx+𝑒Egx+1WEg1x+𝑒Egx+1XE2ndgx+1WEg1x+𝑒Egx+1
390 386 387 388 389 syl3anc φngSxx+11nXE2ndgx+1XE2ndgx+𝑒Egx+1XE2ndgx+𝑒Egx+1WEg1x+𝑒Egx+1XE2ndgx+1WEg1x+𝑒Egx+1
391 384 390 mpand φngSxx+11nXE2ndgx+𝑒Egx+1WEg1x+𝑒Egx+1XE2ndgx+1WEg1x+𝑒Egx+1
392 350 391 syld φngSxx+11nXE2ndgxWEg1xXE2ndgx+1WEg1x+𝑒Egx+1
393 xrex *V
394 393 difexi *−∞V
395 10 24 ressplusg *−∞V+𝑒=+W
396 394 395 ax-mp +𝑒=+W
397 44 ad2antrr φngSxx+11nj1xE:V×V*−∞
398 fzelp1 j1xj1x+1
399 49 ad2antrr φngSxx+11nj1x+1g:1nV×V
400 337 sselda φngSxx+11nj1x+1j1n
401 399 400 ffvelrnd φngSxx+11nj1x+1gjV×V
402 398 401 sylan2 φngSxx+11nj1xgjV×V
403 397 402 ffvelrnd φngSxx+11nj1xEgj*−∞
404 fzp1disj 1xx+1=
405 404 a1i φngSxx+11n1xx+1=
406 disjsn 1xx+1=¬x+11x
407 405 406 sylib φngSxx+11n¬x+11x
408 44 adantr φngSxx+11nE:V×V*−∞
409 408 346 ffvelrnd φngSxx+11nEgx+1*−∞
410 2fveq3 j=x+1Egj=Egx+1
411 64 396 329 330 403 316 407 409 410 gsumunsn φngSxx+11nWj1xx+1Egj=Wj=1xEgj+𝑒Egx+1
412 292 adantr φngSxx+11nEg=j1nEgj
413 412 333 reseq12d φngSxx+11nEg1x+1=j1nEgj1xx+1
414 338 resmptd φngSxx+11nj1nEgj1xx+1=j1xx+1Egj
415 413 414 eqtrd φngSxx+11nEg1x+1=j1xx+1Egj
416 415 oveq2d φngSxx+11nWEg1x+1=Wj1xx+1Egj
417 412 reseq1d φngSxx+11nEg1x=j1nEgj1x
418 339 resmptd φngSxx+11nj1nEgj1x=j1xEgj
419 417 418 eqtrd φngSxx+11nEg1x=j1xEgj
420 419 oveq2d φngSxx+11nWEg1x=Wj=1xEgj
421 420 oveq1d φngSxx+11nWEg1x+𝑒Egx+1=Wj=1xEgj+𝑒Egx+1
422 411 416 421 3eqtr4d φngSxx+11nWEg1x+1=WEg1x+𝑒Egx+1
423 422 breq2d φngSxx+11nXE2ndgx+1WEg1x+1XE2ndgx+1WEg1x+𝑒Egx+1
424 392 423 sylibrd φngSxx+11nXE2ndgxWEg1xXE2ndgx+1WEg1x+1
425 320 424 animpimp2impd xφngSx1nXE2ndgxWEg1xφngSx+11nXE2ndgx+1WEg1x+1
426 244 253 262 271 313 425 nnind nφngSn1nXE2ndgnWEg1n
427 224 426 mpcom φngSn1nXE2ndgnWEg1n
428 226 427 mpd φngSXE2ndgnWEg1n
429 234 428 eqbrtrrd φngSXEYWEg1n
430 ffn Eg:1n*−∞EgFn1n
431 fnresdm EgFn1nEg1n=Eg
432 51 430 431 3syl φngSEg1n=Eg
433 432 oveq2d φngSWEg1n=WEg
434 62 433 eqtr4d φngS𝑠*Eg=WEg1n
435 429 434 breqtrrd φngSXEY𝑠*Eg
436 breq2 p=𝑠*EgXEYpXEY𝑠*Eg
437 435 436 syl5ibrcom φngSp=𝑠*EgXEYp
438 437 rexlimdva φngSp=𝑠*EgXEYp
439 216 438 syl5bi φnprangS𝑠*EgXEYp
440 439 rexlimdva φnprangS𝑠*EgXEYp
441 214 440 syl5bi φpTXEYp
442 441 ralrimiv φpTXEYp
443 infxrgelb T*XEY*XEYsupT*<pTXEYp
444 79 83 443 syl2anc φXEYsupT*<pTXEYp
445 442 444 mpbird φXEYsupT*<
446 81 83 211 445 xrletrid φsupT*<=XEY
447 22 446 eqtrd φFXDFY=XEY