Metamath Proof Explorer

Theorem coemulc

Description: The coefficient function is linear under scalar multiplication. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Assertion coemulc 
|- ( ( A e. CC /\ F e. ( Poly ` S ) ) -> ( coeff ` ( ( CC X. { A } ) oF x. F ) ) = ( ( NN0 X. { A } ) oF x. ( coeff ` F ) ) )

Proof

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 ffvelcdmda 
 |-  ( ( ( 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 ffvelcdm 
 |-  ( ( ( 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 ) ) )