Step |
Hyp |
Ref |
Expression |
1 |
|
ssid |
|- CC C_ CC |
2 |
|
plyconst |
|- ( ( CC C_ CC /\ A e. CC ) -> ( CC X. { A } ) e. ( Poly ` CC ) ) |
3 |
1 2
|
mpan |
|- ( A e. CC -> ( CC X. { A } ) e. ( Poly ` CC ) ) |
4 |
|
plyssc |
|- ( Poly ` S ) C_ ( Poly ` CC ) |
5 |
4
|
sseli |
|- ( F e. ( Poly ` S ) -> F e. ( Poly ` CC ) ) |
6 |
|
plymulcl |
|- ( ( ( CC X. { A } ) e. ( Poly ` CC ) /\ F e. ( Poly ` CC ) ) -> ( ( CC X. { A } ) oF x. F ) e. ( Poly ` CC ) ) |
7 |
3 5 6
|
syl2an |
|- ( ( A e. CC /\ F e. ( Poly ` S ) ) -> ( ( CC X. { A } ) oF x. F ) e. ( Poly ` CC ) ) |
8 |
|
eqid |
|- ( coeff ` ( ( CC X. { A } ) oF x. F ) ) = ( coeff ` ( ( CC X. { A } ) oF x. F ) ) |
9 |
8
|
coef3 |
|- ( ( ( CC X. { A } ) oF x. F ) e. ( Poly ` CC ) -> ( coeff ` ( ( CC X. { A } ) oF x. F ) ) : NN0 --> CC ) |
10 |
|
ffn |
|- ( ( coeff ` ( ( CC X. { A } ) oF x. F ) ) : NN0 --> CC -> ( coeff ` ( ( CC X. { A } ) oF x. F ) ) Fn NN0 ) |
11 |
7 9 10
|
3syl |
|- ( ( A e. CC /\ F e. ( Poly ` S ) ) -> ( coeff ` ( ( CC X. { A } ) oF x. F ) ) Fn NN0 ) |
12 |
|
fconstg |
|- ( A e. CC -> ( NN0 X. { A } ) : NN0 --> { A } ) |
13 |
12
|
adantr |
|- ( ( A e. CC /\ F e. ( Poly ` S ) ) -> ( NN0 X. { A } ) : NN0 --> { A } ) |
14 |
13
|
ffnd |
|- ( ( A e. CC /\ F e. ( Poly ` S ) ) -> ( NN0 X. { A } ) Fn NN0 ) |
15 |
|
eqid |
|- ( coeff ` F ) = ( coeff ` F ) |
16 |
15
|
coef3 |
|- ( F e. ( Poly ` S ) -> ( coeff ` F ) : NN0 --> CC ) |
17 |
16
|
adantl |
|- ( ( A e. CC /\ F e. ( Poly ` S ) ) -> ( coeff ` F ) : NN0 --> CC ) |
18 |
17
|
ffnd |
|- ( ( A e. CC /\ F e. ( Poly ` S ) ) -> ( coeff ` F ) Fn NN0 ) |
19 |
|
nn0ex |
|- NN0 e. _V |
20 |
19
|
a1i |
|- ( ( A e. CC /\ F e. ( Poly ` S ) ) -> NN0 e. _V ) |
21 |
|
inidm |
|- ( NN0 i^i NN0 ) = NN0 |
22 |
14 18 20 20 21
|
offn |
|- ( ( A e. CC /\ F e. ( Poly ` S ) ) -> ( ( NN0 X. { A } ) oF x. ( coeff ` F ) ) Fn NN0 ) |
23 |
3
|
ad2antrr |
|- ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( CC X. { A } ) e. ( Poly ` CC ) ) |
24 |
|
eqid |
|- ( coeff ` ( CC X. { A } ) ) = ( coeff ` ( CC X. { A } ) ) |
25 |
24
|
coefv0 |
|- ( ( CC X. { A } ) e. ( Poly ` CC ) -> ( ( CC X. { A } ) ` 0 ) = ( ( coeff ` ( CC X. { A } ) ) ` 0 ) ) |
26 |
23 25
|
syl |
|- ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( ( CC X. { A } ) ` 0 ) = ( ( coeff ` ( CC X. { A } ) ) ` 0 ) ) |
27 |
|
simpll |
|- ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> A e. CC ) |
28 |
|
0cn |
|- 0 e. CC |
29 |
|
fvconst2g |
|- ( ( A e. CC /\ 0 e. CC ) -> ( ( CC X. { A } ) ` 0 ) = A ) |
30 |
27 28 29
|
sylancl |
|- ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( ( CC X. { A } ) ` 0 ) = A ) |
31 |
26 30
|
eqtr3d |
|- ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( ( coeff ` ( CC X. { A } ) ) ` 0 ) = A ) |
32 |
|
simpr |
|- ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> n e. NN0 ) |
33 |
32
|
nn0cnd |
|- ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> n e. CC ) |
34 |
33
|
subid1d |
|- ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( n - 0 ) = n ) |
35 |
34
|
fveq2d |
|- ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( ( coeff ` F ) ` ( n - 0 ) ) = ( ( coeff ` F ) ` n ) ) |
36 |
31 35
|
oveq12d |
|- ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( ( ( coeff ` ( CC X. { A } ) ) ` 0 ) x. ( ( coeff ` F ) ` ( n - 0 ) ) ) = ( A x. ( ( coeff ` F ) ` n ) ) ) |
37 |
5
|
ad2antlr |
|- ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> F e. ( Poly ` CC ) ) |
38 |
24 15
|
coemul |
|- ( ( ( CC X. { A } ) e. ( Poly ` CC ) /\ F e. ( Poly ` CC ) /\ n e. NN0 ) -> ( ( coeff ` ( ( CC X. { A } ) oF x. F ) ) ` n ) = sum_ k e. ( 0 ... n ) ( ( ( coeff ` ( CC X. { A } ) ) ` k ) x. ( ( coeff ` F ) ` ( n - k ) ) ) ) |
39 |
23 37 32 38
|
syl3anc |
|- ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( ( coeff ` ( ( CC X. { A } ) oF x. F ) ) ` n ) = sum_ k e. ( 0 ... n ) ( ( ( coeff ` ( CC X. { A } ) ) ` k ) x. ( ( coeff ` F ) ` ( n - k ) ) ) ) |
40 |
|
nn0uz |
|- NN0 = ( ZZ>= ` 0 ) |
41 |
32 40
|
eleqtrdi |
|- ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> n e. ( ZZ>= ` 0 ) ) |
42 |
|
fzss2 |
|- ( n e. ( ZZ>= ` 0 ) -> ( 0 ... 0 ) C_ ( 0 ... n ) ) |
43 |
41 42
|
syl |
|- ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( 0 ... 0 ) C_ ( 0 ... n ) ) |
44 |
|
elfz1eq |
|- ( k e. ( 0 ... 0 ) -> k = 0 ) |
45 |
44
|
adantl |
|- ( ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) /\ k e. ( 0 ... 0 ) ) -> k = 0 ) |
46 |
|
fveq2 |
|- ( k = 0 -> ( ( coeff ` ( CC X. { A } ) ) ` k ) = ( ( coeff ` ( CC X. { A } ) ) ` 0 ) ) |
47 |
|
oveq2 |
|- ( k = 0 -> ( n - k ) = ( n - 0 ) ) |
48 |
47
|
fveq2d |
|- ( k = 0 -> ( ( coeff ` F ) ` ( n - k ) ) = ( ( coeff ` F ) ` ( n - 0 ) ) ) |
49 |
46 48
|
oveq12d |
|- ( k = 0 -> ( ( ( coeff ` ( CC X. { A } ) ) ` k ) x. ( ( coeff ` F ) ` ( n - k ) ) ) = ( ( ( coeff ` ( CC X. { A } ) ) ` 0 ) x. ( ( coeff ` F ) ` ( n - 0 ) ) ) ) |
50 |
45 49
|
syl |
|- ( ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) /\ k e. ( 0 ... 0 ) ) -> ( ( ( coeff ` ( CC X. { A } ) ) ` k ) x. ( ( coeff ` F ) ` ( n - k ) ) ) = ( ( ( coeff ` ( CC X. { A } ) ) ` 0 ) x. ( ( coeff ` F ) ` ( n - 0 ) ) ) ) |
51 |
17
|
ffvelrnda |
|- ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( ( coeff ` F ) ` n ) e. CC ) |
52 |
27 51
|
mulcld |
|- ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( A x. ( ( coeff ` F ) ` n ) ) e. CC ) |
53 |
36 52
|
eqeltrd |
|- ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( ( ( coeff ` ( CC X. { A } ) ) ` 0 ) x. ( ( coeff ` F ) ` ( n - 0 ) ) ) e. CC ) |
54 |
53
|
adantr |
|- ( ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) /\ k e. ( 0 ... 0 ) ) -> ( ( ( coeff ` ( CC X. { A } ) ) ` 0 ) x. ( ( coeff ` F ) ` ( n - 0 ) ) ) e. CC ) |
55 |
50 54
|
eqeltrd |
|- ( ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) /\ k e. ( 0 ... 0 ) ) -> ( ( ( coeff ` ( CC X. { A } ) ) ` k ) x. ( ( coeff ` F ) ` ( n - k ) ) ) e. CC ) |
56 |
|
eldifn |
|- ( k e. ( ( 0 ... n ) \ ( 0 ... 0 ) ) -> -. k e. ( 0 ... 0 ) ) |
57 |
56
|
adantl |
|- ( ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) /\ k e. ( ( 0 ... n ) \ ( 0 ... 0 ) ) ) -> -. k e. ( 0 ... 0 ) ) |
58 |
|
eldifi |
|- ( k e. ( ( 0 ... n ) \ ( 0 ... 0 ) ) -> k e. ( 0 ... n ) ) |
59 |
|
elfznn0 |
|- ( k e. ( 0 ... n ) -> k e. NN0 ) |
60 |
58 59
|
syl |
|- ( k e. ( ( 0 ... n ) \ ( 0 ... 0 ) ) -> k e. NN0 ) |
61 |
|
eqid |
|- ( deg ` ( CC X. { A } ) ) = ( deg ` ( CC X. { A } ) ) |
62 |
24 61
|
dgrub |
|- ( ( ( CC X. { A } ) e. ( Poly ` CC ) /\ k e. NN0 /\ ( ( coeff ` ( CC X. { A } ) ) ` k ) =/= 0 ) -> k <_ ( deg ` ( CC X. { A } ) ) ) |
63 |
62
|
3expia |
|- ( ( ( CC X. { A } ) e. ( Poly ` CC ) /\ k e. NN0 ) -> ( ( ( coeff ` ( CC X. { A } ) ) ` k ) =/= 0 -> k <_ ( deg ` ( CC X. { A } ) ) ) ) |
64 |
23 60 63
|
syl2an |
|- ( ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) /\ k e. ( ( 0 ... n ) \ ( 0 ... 0 ) ) ) -> ( ( ( coeff ` ( CC X. { A } ) ) ` k ) =/= 0 -> k <_ ( deg ` ( CC X. { A } ) ) ) ) |
65 |
|
0dgr |
|- ( A e. CC -> ( deg ` ( CC X. { A } ) ) = 0 ) |
66 |
65
|
ad3antrrr |
|- ( ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) /\ k e. ( ( 0 ... n ) \ ( 0 ... 0 ) ) ) -> ( deg ` ( CC X. { A } ) ) = 0 ) |
67 |
66
|
breq2d |
|- ( ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) /\ k e. ( ( 0 ... n ) \ ( 0 ... 0 ) ) ) -> ( k <_ ( deg ` ( CC X. { A } ) ) <-> k <_ 0 ) ) |
68 |
60
|
adantl |
|- ( ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) /\ k e. ( ( 0 ... n ) \ ( 0 ... 0 ) ) ) -> k e. NN0 ) |
69 |
|
nn0le0eq0 |
|- ( k e. NN0 -> ( k <_ 0 <-> k = 0 ) ) |
70 |
68 69
|
syl |
|- ( ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) /\ k e. ( ( 0 ... n ) \ ( 0 ... 0 ) ) ) -> ( k <_ 0 <-> k = 0 ) ) |
71 |
67 70
|
bitrd |
|- ( ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) /\ k e. ( ( 0 ... n ) \ ( 0 ... 0 ) ) ) -> ( k <_ ( deg ` ( CC X. { A } ) ) <-> k = 0 ) ) |
72 |
64 71
|
sylibd |
|- ( ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) /\ k e. ( ( 0 ... n ) \ ( 0 ... 0 ) ) ) -> ( ( ( coeff ` ( CC X. { A } ) ) ` k ) =/= 0 -> k = 0 ) ) |
73 |
|
id |
|- ( k = 0 -> k = 0 ) |
74 |
|
0z |
|- 0 e. ZZ |
75 |
|
elfz3 |
|- ( 0 e. ZZ -> 0 e. ( 0 ... 0 ) ) |
76 |
74 75
|
ax-mp |
|- 0 e. ( 0 ... 0 ) |
77 |
73 76
|
eqeltrdi |
|- ( k = 0 -> k e. ( 0 ... 0 ) ) |
78 |
72 77
|
syl6 |
|- ( ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) /\ k e. ( ( 0 ... n ) \ ( 0 ... 0 ) ) ) -> ( ( ( coeff ` ( CC X. { A } ) ) ` k ) =/= 0 -> k e. ( 0 ... 0 ) ) ) |
79 |
78
|
necon1bd |
|- ( ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) /\ k e. ( ( 0 ... n ) \ ( 0 ... 0 ) ) ) -> ( -. k e. ( 0 ... 0 ) -> ( ( coeff ` ( CC X. { A } ) ) ` k ) = 0 ) ) |
80 |
57 79
|
mpd |
|- ( ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) /\ k e. ( ( 0 ... n ) \ ( 0 ... 0 ) ) ) -> ( ( coeff ` ( CC X. { A } ) ) ` k ) = 0 ) |
81 |
80
|
oveq1d |
|- ( ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) /\ k e. ( ( 0 ... n ) \ ( 0 ... 0 ) ) ) -> ( ( ( coeff ` ( CC X. { A } ) ) ` k ) x. ( ( coeff ` F ) ` ( n - k ) ) ) = ( 0 x. ( ( coeff ` F ) ` ( n - k ) ) ) ) |
82 |
17
|
adantr |
|- ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( coeff ` F ) : NN0 --> CC ) |
83 |
|
fznn0sub |
|- ( k e. ( 0 ... n ) -> ( n - k ) e. NN0 ) |
84 |
58 83
|
syl |
|- ( k e. ( ( 0 ... n ) \ ( 0 ... 0 ) ) -> ( n - k ) e. NN0 ) |
85 |
|
ffvelrn |
|- ( ( ( coeff ` F ) : NN0 --> CC /\ ( n - k ) e. NN0 ) -> ( ( coeff ` F ) ` ( n - k ) ) e. CC ) |
86 |
82 84 85
|
syl2an |
|- ( ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) /\ k e. ( ( 0 ... n ) \ ( 0 ... 0 ) ) ) -> ( ( coeff ` F ) ` ( n - k ) ) e. CC ) |
87 |
86
|
mul02d |
|- ( ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) /\ k e. ( ( 0 ... n ) \ ( 0 ... 0 ) ) ) -> ( 0 x. ( ( coeff ` F ) ` ( n - k ) ) ) = 0 ) |
88 |
81 87
|
eqtrd |
|- ( ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) /\ k e. ( ( 0 ... n ) \ ( 0 ... 0 ) ) ) -> ( ( ( coeff ` ( CC X. { A } ) ) ` k ) x. ( ( coeff ` F ) ` ( n - k ) ) ) = 0 ) |
89 |
|
fzfid |
|- ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( 0 ... n ) e. Fin ) |
90 |
43 55 88 89
|
fsumss |
|- ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> sum_ k e. ( 0 ... 0 ) ( ( ( coeff ` ( CC X. { A } ) ) ` k ) x. ( ( coeff ` F ) ` ( n - k ) ) ) = sum_ k e. ( 0 ... n ) ( ( ( coeff ` ( CC X. { A } ) ) ` k ) x. ( ( coeff ` F ) ` ( n - k ) ) ) ) |
91 |
49
|
fsum1 |
|- ( ( 0 e. ZZ /\ ( ( ( coeff ` ( CC X. { A } ) ) ` 0 ) x. ( ( coeff ` F ) ` ( n - 0 ) ) ) e. CC ) -> sum_ k e. ( 0 ... 0 ) ( ( ( coeff ` ( CC X. { A } ) ) ` k ) x. ( ( coeff ` F ) ` ( n - k ) ) ) = ( ( ( coeff ` ( CC X. { A } ) ) ` 0 ) x. ( ( coeff ` F ) ` ( n - 0 ) ) ) ) |
92 |
74 53 91
|
sylancr |
|- ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> sum_ k e. ( 0 ... 0 ) ( ( ( coeff ` ( CC X. { A } ) ) ` k ) x. ( ( coeff ` F ) ` ( n - k ) ) ) = ( ( ( coeff ` ( CC X. { A } ) ) ` 0 ) x. ( ( coeff ` F ) ` ( n - 0 ) ) ) ) |
93 |
39 90 92
|
3eqtr2d |
|- ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( ( coeff ` ( ( CC X. { A } ) oF x. F ) ) ` n ) = ( ( ( coeff ` ( CC X. { A } ) ) ` 0 ) x. ( ( coeff ` F ) ` ( n - 0 ) ) ) ) |
94 |
|
simpl |
|- ( ( A e. CC /\ F e. ( Poly ` S ) ) -> A e. CC ) |
95 |
|
eqidd |
|- ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( ( coeff ` F ) ` n ) = ( ( coeff ` F ) ` n ) ) |
96 |
20 94 18 95
|
ofc1 |
|- ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( ( ( NN0 X. { A } ) oF x. ( coeff ` F ) ) ` n ) = ( A x. ( ( coeff ` F ) ` n ) ) ) |
97 |
36 93 96
|
3eqtr4d |
|- ( ( ( A e. CC /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( ( coeff ` ( ( CC X. { A } ) oF x. F ) ) ` n ) = ( ( ( NN0 X. { A } ) oF x. ( coeff ` F ) ) ` n ) ) |
98 |
11 22 97
|
eqfnfvd |
|- ( ( A e. CC /\ F e. ( Poly ` S ) ) -> ( coeff ` ( ( CC X. { A } ) oF x. F ) ) = ( ( NN0 X. { A } ) oF x. ( coeff ` F ) ) ) |