| Step |
Hyp |
Ref |
Expression |
| 1 |
|
plycj.2 |
|- G = ( ( * o. F ) o. * ) |
| 2 |
|
coecj.3 |
|- A = ( coeff ` F ) |
| 3 |
|
cjcl |
|- ( x e. CC -> ( * ` x ) e. CC ) |
| 4 |
3
|
adantl |
|- ( ( F e. ( Poly ` S ) /\ x e. CC ) -> ( * ` x ) e. CC ) |
| 5 |
|
plyssc |
|- ( Poly ` S ) C_ ( Poly ` CC ) |
| 6 |
5
|
sseli |
|- ( F e. ( Poly ` S ) -> F e. ( Poly ` CC ) ) |
| 7 |
1 4 6
|
plycj |
|- ( F e. ( Poly ` S ) -> G e. ( Poly ` CC ) ) |
| 8 |
|
dgrcl |
|- ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 ) |
| 9 |
|
cjf |
|- * : CC --> CC |
| 10 |
2
|
coef3 |
|- ( F e. ( Poly ` S ) -> A : NN0 --> CC ) |
| 11 |
|
fco |
|- ( ( * : CC --> CC /\ A : NN0 --> CC ) -> ( * o. A ) : NN0 --> CC ) |
| 12 |
9 10 11
|
sylancr |
|- ( F e. ( Poly ` S ) -> ( * o. A ) : NN0 --> CC ) |
| 13 |
|
fvco3 |
|- ( ( A : NN0 --> CC /\ k e. NN0 ) -> ( ( * o. A ) ` k ) = ( * ` ( A ` k ) ) ) |
| 14 |
10 13
|
sylan |
|- ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> ( ( * o. A ) ` k ) = ( * ` ( A ` k ) ) ) |
| 15 |
|
cj0 |
|- ( * ` 0 ) = 0 |
| 16 |
15
|
eqcomi |
|- 0 = ( * ` 0 ) |
| 17 |
16
|
a1i |
|- ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> 0 = ( * ` 0 ) ) |
| 18 |
14 17
|
eqeq12d |
|- ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> ( ( ( * o. A ) ` k ) = 0 <-> ( * ` ( A ` k ) ) = ( * ` 0 ) ) ) |
| 19 |
10
|
ffvelcdmda |
|- ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> ( A ` k ) e. CC ) |
| 20 |
|
0cnd |
|- ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> 0 e. CC ) |
| 21 |
|
cj11 |
|- ( ( ( A ` k ) e. CC /\ 0 e. CC ) -> ( ( * ` ( A ` k ) ) = ( * ` 0 ) <-> ( A ` k ) = 0 ) ) |
| 22 |
19 20 21
|
syl2anc |
|- ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> ( ( * ` ( A ` k ) ) = ( * ` 0 ) <-> ( A ` k ) = 0 ) ) |
| 23 |
18 22
|
bitrd |
|- ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> ( ( ( * o. A ) ` k ) = 0 <-> ( A ` k ) = 0 ) ) |
| 24 |
23
|
necon3bid |
|- ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> ( ( ( * o. A ) ` k ) =/= 0 <-> ( A ` k ) =/= 0 ) ) |
| 25 |
|
eqid |
|- ( deg ` F ) = ( deg ` F ) |
| 26 |
2 25
|
dgrub2 |
|- ( F e. ( Poly ` S ) -> ( A " ( ZZ>= ` ( ( deg ` F ) + 1 ) ) ) = { 0 } ) |
| 27 |
|
plyco0 |
|- ( ( ( deg ` F ) e. NN0 /\ A : NN0 --> CC ) -> ( ( A " ( ZZ>= ` ( ( deg ` F ) + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ ( deg ` F ) ) ) ) |
| 28 |
8 10 27
|
syl2anc |
|- ( F e. ( Poly ` S ) -> ( ( A " ( ZZ>= ` ( ( deg ` F ) + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ ( deg ` F ) ) ) ) |
| 29 |
26 28
|
mpbid |
|- ( F e. ( Poly ` S ) -> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ ( deg ` F ) ) ) |
| 30 |
29
|
r19.21bi |
|- ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> ( ( A ` k ) =/= 0 -> k <_ ( deg ` F ) ) ) |
| 31 |
24 30
|
sylbid |
|- ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> ( ( ( * o. A ) ` k ) =/= 0 -> k <_ ( deg ` F ) ) ) |
| 32 |
31
|
ralrimiva |
|- ( F e. ( Poly ` S ) -> A. k e. NN0 ( ( ( * o. A ) ` k ) =/= 0 -> k <_ ( deg ` F ) ) ) |
| 33 |
|
plyco0 |
|- ( ( ( deg ` F ) e. NN0 /\ ( * o. A ) : NN0 --> CC ) -> ( ( ( * o. A ) " ( ZZ>= ` ( ( deg ` F ) + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( ( * o. A ) ` k ) =/= 0 -> k <_ ( deg ` F ) ) ) ) |
| 34 |
8 12 33
|
syl2anc |
|- ( F e. ( Poly ` S ) -> ( ( ( * o. A ) " ( ZZ>= ` ( ( deg ` F ) + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( ( * o. A ) ` k ) =/= 0 -> k <_ ( deg ` F ) ) ) ) |
| 35 |
32 34
|
mpbird |
|- ( F e. ( Poly ` S ) -> ( ( * o. A ) " ( ZZ>= ` ( ( deg ` F ) + 1 ) ) ) = { 0 } ) |
| 36 |
25 1 2
|
plycjlem |
|- ( F e. ( Poly ` S ) -> G = ( y e. CC |-> sum_ z e. ( 0 ... ( deg ` F ) ) ( ( ( * o. A ) ` z ) x. ( y ^ z ) ) ) ) |
| 37 |
7 8 12 35 36
|
coeeq |
|- ( F e. ( Poly ` S ) -> ( coeff ` G ) = ( * o. A ) ) |