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 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 ) ) )