Metamath Proof Explorer


Theorem elply2

Description: The coefficient function can be assumed to have zeroes outside 0 ... n . (Contributed by Mario Carneiro, 20-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Assertion elply2 FPolySSn0aS00an+1=0F=zk=0nakzk

Proof

Step Hyp Ref Expression
1 elply FPolySSn0fS00F=zk=0nfkzk
2 simpr Sn0fS00fS00
3 simpll Sn0fS00S
4 cnex V
5 ssexg SVSV
6 3 4 5 sylancl Sn0fS00SV
7 snex 0V
8 unexg SV0VS0V
9 6 7 8 sylancl Sn0fS00S0V
10 nn0ex 0V
11 elmapg S0V0VfS00f:0S0
12 9 10 11 sylancl Sn0fS00fS00f:0S0
13 2 12 mpbid Sn0fS00f:0S0
14 13 ffvelrnda Sn0fS00x0fxS0
15 ssun2 0S0
16 c0ex 0V
17 16 snss 0S00S0
18 15 17 mpbir 0S0
19 ifcl fxS00S0ifx0nfx0S0
20 14 18 19 sylancl Sn0fS00x0ifx0nfx0S0
21 20 fmpttd Sn0fS00x0ifx0nfx0:0S0
22 elmapg S0V0Vx0ifx0nfx0S00x0ifx0nfx0:0S0
23 9 10 22 sylancl Sn0fS00x0ifx0nfx0S00x0ifx0nfx0:0S0
24 21 23 mpbird Sn0fS00x0ifx0nfx0S00
25 eleq1w x=kx0nk0n
26 fveq2 x=kfx=fk
27 25 26 ifbieq1d x=kifx0nfx0=ifk0nfk0
28 eqid x0ifx0nfx0=x0ifx0nfx0
29 fvex fkV
30 29 16 ifex ifk0nfk0V
31 27 28 30 fvmpt k0x0ifx0nfx0k=ifk0nfk0
32 31 ad2antll Sn0fS00k0x0ifx0nfx0k=ifk0nfk0
33 iffalse ¬k0nifk0nfk0=0
34 33 eqeq2d ¬k0nx0ifx0nfx0k=ifk0nfk0x0ifx0nfx0k=0
35 32 34 syl5ibcom Sn0fS00k0¬k0nx0ifx0nfx0k=0
36 35 necon1ad Sn0fS00k0x0ifx0nfx0k0k0n
37 elfzle2 k0nkn
38 36 37 syl6 Sn0fS00k0x0ifx0nfx0k0kn
39 38 anassrs Sn0fS00k0x0ifx0nfx0k0kn
40 39 ralrimiva Sn0fS00k0x0ifx0nfx0k0kn
41 simplr Sn0fS00n0
42 0cnd Sn0fS000
43 42 snssd Sn0fS000
44 3 43 unssd Sn0fS00S0
45 21 44 fssd Sn0fS00x0ifx0nfx0:0
46 plyco0 n0x0ifx0nfx0:0x0ifx0nfx0n+1=0k0x0ifx0nfx0k0kn
47 41 45 46 syl2anc Sn0fS00x0ifx0nfx0n+1=0k0x0ifx0nfx0k0kn
48 40 47 mpbird Sn0fS00x0ifx0nfx0n+1=0
49 eqidd Sn0fS00zk=0nfkzk=zk=0nfkzk
50 imaeq1 a=x0ifx0nfx0an+1=x0ifx0nfx0n+1
51 50 eqeq1d a=x0ifx0nfx0an+1=0x0ifx0nfx0n+1=0
52 fveq1 a=x0ifx0nfx0ak=x0ifx0nfx0k
53 elfznn0 k0nk0
54 53 31 syl k0nx0ifx0nfx0k=ifk0nfk0
55 iftrue k0nifk0nfk0=fk
56 54 55 eqtrd k0nx0ifx0nfx0k=fk
57 52 56 sylan9eq a=x0ifx0nfx0k0nak=fk
58 57 oveq1d a=x0ifx0nfx0k0nakzk=fkzk
59 58 sumeq2dv a=x0ifx0nfx0k=0nakzk=k=0nfkzk
60 59 mpteq2dv a=x0ifx0nfx0zk=0nakzk=zk=0nfkzk
61 60 eqeq2d a=x0ifx0nfx0zk=0nfkzk=zk=0nakzkzk=0nfkzk=zk=0nfkzk
62 51 61 anbi12d a=x0ifx0nfx0an+1=0zk=0nfkzk=zk=0nakzkx0ifx0nfx0n+1=0zk=0nfkzk=zk=0nfkzk
63 62 rspcev x0ifx0nfx0S00x0ifx0nfx0n+1=0zk=0nfkzk=zk=0nfkzkaS00an+1=0zk=0nfkzk=zk=0nakzk
64 24 48 49 63 syl12anc Sn0fS00aS00an+1=0zk=0nfkzk=zk=0nakzk
65 eqeq1 F=zk=0nfkzkF=zk=0nakzkzk=0nfkzk=zk=0nakzk
66 65 anbi2d F=zk=0nfkzkan+1=0F=zk=0nakzkan+1=0zk=0nfkzk=zk=0nakzk
67 66 rexbidv F=zk=0nfkzkaS00an+1=0F=zk=0nakzkaS00an+1=0zk=0nfkzk=zk=0nakzk
68 64 67 syl5ibrcom Sn0fS00F=zk=0nfkzkaS00an+1=0F=zk=0nakzk
69 68 rexlimdva Sn0fS00F=zk=0nfkzkaS00an+1=0F=zk=0nakzk
70 69 reximdva Sn0fS00F=zk=0nfkzkn0aS00an+1=0F=zk=0nakzk
71 70 imdistani Sn0fS00F=zk=0nfkzkSn0aS00an+1=0F=zk=0nakzk
72 1 71 sylbi FPolySSn0aS00an+1=0F=zk=0nakzk
73 simpr an+1=0F=zk=0nakzkF=zk=0nakzk
74 73 reximi aS00an+1=0F=zk=0nakzkaS00F=zk=0nakzk
75 74 reximi n0aS00an+1=0F=zk=0nakzkn0aS00F=zk=0nakzk
76 75 anim2i Sn0aS00an+1=0F=zk=0nakzkSn0aS00F=zk=0nakzk
77 elply FPolySSn0aS00F=zk=0nakzk
78 76 77 sylibr Sn0aS00an+1=0F=zk=0nakzkFPolyS
79 72 78 impbii FPolySSn0aS00an+1=0F=zk=0nakzk