Metamath Proof Explorer


Theorem elplyd

Description: Sufficient condition for elementhood in the set of polynomials. (Contributed by Mario Carneiro, 17-Jul-2014)

Ref Expression
Hypotheses elplyd.1 φS
elplyd.2 φN0
elplyd.3 φk0NAS
Assertion elplyd φzk=0NAzkPolyS

Proof

Step Hyp Ref Expression
1 elplyd.1 φS
2 elplyd.2 φN0
3 elplyd.3 φk0NAS
4 nffvmpt1 _kk0ifk0NA0j
5 nfcv _k×
6 nfcv _kzj
7 4 5 6 nfov _kk0ifk0NA0jzj
8 nfcv _jk0ifk0NA0kzk
9 fveq2 j=kk0ifk0NA0j=k0ifk0NA0k
10 oveq2 j=kzj=zk
11 9 10 oveq12d j=kk0ifk0NA0jzj=k0ifk0NA0kzk
12 7 8 11 cbvsumi j=0Nk0ifk0NA0jzj=k=0Nk0ifk0NA0kzk
13 elfznn0 k0Nk0
14 iftrue k0Nifk0NA0=A
15 14 adantl φk0Nifk0NA0=A
16 15 3 eqeltrd φk0Nifk0NA0S
17 eqid k0ifk0NA0=k0ifk0NA0
18 17 fvmpt2 k0ifk0NA0Sk0ifk0NA0k=ifk0NA0
19 13 16 18 syl2an2 φk0Nk0ifk0NA0k=ifk0NA0
20 19 15 eqtrd φk0Nk0ifk0NA0k=A
21 20 oveq1d φk0Nk0ifk0NA0kzk=Azk
22 21 sumeq2dv φk=0Nk0ifk0NA0kzk=k=0NAzk
23 12 22 eqtrid φj=0Nk0ifk0NA0jzj=k=0NAzk
24 23 mpteq2dv φzj=0Nk0ifk0NA0jzj=zk=0NAzk
25 0cnd φ0
26 25 snssd φ0
27 1 26 unssd φS0
28 elun1 ASAS0
29 3 28 syl φk0NAS0
30 29 adantlr φk0k0NAS0
31 ssun2 0S0
32 c0ex 0V
33 32 snss 0S00S0
34 31 33 mpbir 0S0
35 34 a1i φk0¬k0N0S0
36 30 35 ifclda φk0ifk0NA0S0
37 36 fmpttd φk0ifk0NA0:0S0
38 elplyr S0N0k0ifk0NA0:0S0zj=0Nk0ifk0NA0jzjPolyS0
39 27 2 37 38 syl3anc φzj=0Nk0ifk0NA0jzjPolyS0
40 24 39 eqeltrrd φzk=0NAzkPolyS0
41 plyun0 PolyS0=PolyS
42 40 41 eleqtrdi φzk=0NAzkPolyS