Metamath Proof Explorer

Theorem plycjlem

Description: Lemma for plycj and coecj . (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses plycjlem.1 
|- N = ( deg ` F )
plycjlem.2 
|- G = ( ( * o. F ) o. * )
plycjlem.3 
|- A = ( coeff ` F )
Assertion plycjlem 
|- ( F e. ( Poly ` S ) -> G = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( * o. A ) ` k ) x. ( z ^ k ) ) ) )

Proof

Step Hyp Ref Expression
1 plycjlem.1 
 |-  N = ( deg ` F )
2 plycjlem.2 
 |-  G = ( ( * o. F ) o. * )
3 plycjlem.3 
 |-  A = ( coeff ` F )
4 cjcl 
 |-  ( z e. CC -> ( * ` z ) e. CC )
5 4 adantl 
 |-  ( ( F e. ( Poly ` S ) /\ z e. CC ) -> ( * ` z ) e. CC )
6 cjf 
 |-  * : CC --> CC
7 6 a1i 
 |-  ( F e. ( Poly ` S ) -> * : CC --> CC )
8 7 feqmptd 
 |-  ( F e. ( Poly ` S ) -> * = ( z e. CC |-> ( * ` z ) ) )
9 fzfid 
 |-  ( ( F e. ( Poly ` S ) /\ x e. CC ) -> ( 0 ... N ) e. Fin )
10 3 coef3 
 |-  ( F e. ( Poly ` S ) -> A : NN0 --> CC )
11 10 adantr 
 |-  ( ( F e. ( Poly ` S ) /\ x e. CC ) -> A : NN0 --> CC )
12 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
13 ffvelcdm 
 |-  ( ( A : NN0 --> CC /\ k e. NN0 ) -> ( A ` k ) e. CC )
14 11 12 13 syl2an 
 |-  ( ( ( F e. ( Poly ` S ) /\ x e. CC ) /\ k e. ( 0 ... N ) ) -> ( A ` k ) e. CC )
15 expcl 
 |-  ( ( x e. CC /\ k e. NN0 ) -> ( x ^ k ) e. CC )
16 12 15 sylan2 
 |-  ( ( x e. CC /\ k e. ( 0 ... N ) ) -> ( x ^ k ) e. CC )
17 16 adantll 
 |-  ( ( ( F e. ( Poly ` S ) /\ x e. CC ) /\ k e. ( 0 ... N ) ) -> ( x ^ k ) e. CC )
18 14 17 mulcld 
 |-  ( ( ( F e. ( Poly ` S ) /\ x e. CC ) /\ k e. ( 0 ... N ) ) -> ( ( A ` k ) x. ( x ^ k ) ) e. CC )
19 9 18 fsumcl 
 |-  ( ( F e. ( Poly ` S ) /\ x e. CC ) -> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( x ^ k ) ) e. CC )
20 3 1 coeid 
 |-  ( F e. ( Poly ` S ) -> F = ( x e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( x ^ k ) ) ) )
21 fveq2 
 |-  ( z = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( x ^ k ) ) -> ( * ` z ) = ( * ` sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( x ^ k ) ) ) )
22 19 20 8 21 fmptco 
 |-  ( F e. ( Poly ` S ) -> ( * o. F ) = ( x e. CC |-> ( * ` sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( x ^ k ) ) ) ) )
23 oveq1 
 |-  ( x = ( * ` z ) -> ( x ^ k ) = ( ( * ` z ) ^ k ) )
24 23 oveq2d 
 |-  ( x = ( * ` z ) -> ( ( A ` k ) x. ( x ^ k ) ) = ( ( A ` k ) x. ( ( * ` z ) ^ k ) ) )
25 24 sumeq2sdv 
 |-  ( x = ( * ` z ) -> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( x ^ k ) ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( ( * ` z ) ^ k ) ) )
26 25 fveq2d 
 |-  ( x = ( * ` z ) -> ( * ` sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( x ^ k ) ) ) = ( * ` sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( ( * ` z ) ^ k ) ) ) )
27 5 8 22 26 fmptco 
 |-  ( F e. ( Poly ` S ) -> ( ( * o. F ) o. * ) = ( z e. CC |-> ( * ` sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( ( * ` z ) ^ k ) ) ) ) )
28 2 27 eqtrid 
 |-  ( F e. ( Poly ` S ) -> G = ( z e. CC |-> ( * ` sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( ( * ` z ) ^ k ) ) ) ) )
29 fzfid 
 |-  ( ( F e. ( Poly ` S ) /\ z e. CC ) -> ( 0 ... N ) e. Fin )
30 10 adantr 
 |-  ( ( F e. ( Poly ` S ) /\ z e. CC ) -> A : NN0 --> CC )
31 30 12 13 syl2an 
 |-  ( ( ( F e. ( Poly ` S ) /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> ( A ` k ) e. CC )
32 expcl 
 |-  ( ( ( * ` z ) e. CC /\ k e. NN0 ) -> ( ( * ` z ) ^ k ) e. CC )
33 5 12 32 syl2an 
 |-  ( ( ( F e. ( Poly ` S ) /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> ( ( * ` z ) ^ k ) e. CC )
34 31 33 mulcld 
 |-  ( ( ( F e. ( Poly ` S ) /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> ( ( A ` k ) x. ( ( * ` z ) ^ k ) ) e. CC )
35 29 34 fsumcj 
 |-  ( ( F e. ( Poly ` S ) /\ z e. CC ) -> ( * ` sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( ( * ` z ) ^ k ) ) ) = sum_ k e. ( 0 ... N ) ( * ` ( ( A ` k ) x. ( ( * ` z ) ^ k ) ) ) )
36 31 33 cjmuld 
 |-  ( ( ( F e. ( Poly ` S ) /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> ( * ` ( ( A ` k ) x. ( ( * ` z ) ^ k ) ) ) = ( ( * ` ( A ` k ) ) x. ( * ` ( ( * ` z ) ^ k ) ) ) )
37 fvco3 
 |-  ( ( A : NN0 --> CC /\ k e. NN0 ) -> ( ( * o. A ) ` k ) = ( * ` ( A ` k ) ) )
38 30 12 37 syl2an 
 |-  ( ( ( F e. ( Poly ` S ) /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> ( ( * o. A ) ` k ) = ( * ` ( A ` k ) ) )
39 cjexp 
 |-  ( ( ( * ` z ) e. CC /\ k e. NN0 ) -> ( * ` ( ( * ` z ) ^ k ) ) = ( ( * ` ( * ` z ) ) ^ k ) )
40 5 12 39 syl2an 
 |-  ( ( ( F e. ( Poly ` S ) /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> ( * ` ( ( * ` z ) ^ k ) ) = ( ( * ` ( * ` z ) ) ^ k ) )
41 cjcj 
 |-  ( z e. CC -> ( * ` ( * ` z ) ) = z )
42 41 ad2antlr 
 |-  ( ( ( F e. ( Poly ` S ) /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> ( * ` ( * ` z ) ) = z )
43 42 oveq1d 
 |-  ( ( ( F e. ( Poly ` S ) /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> ( ( * ` ( * ` z ) ) ^ k ) = ( z ^ k ) )
44 40 43 eqtr2d 
 |-  ( ( ( F e. ( Poly ` S ) /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> ( z ^ k ) = ( * ` ( ( * ` z ) ^ k ) ) )
45 38 44 oveq12d 
 |-  ( ( ( F e. ( Poly ` S ) /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> ( ( ( * o. A ) ` k ) x. ( z ^ k ) ) = ( ( * ` ( A ` k ) ) x. ( * ` ( ( * ` z ) ^ k ) ) ) )
46 36 45 eqtr4d 
 |-  ( ( ( F e. ( Poly ` S ) /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> ( * ` ( ( A ` k ) x. ( ( * ` z ) ^ k ) ) ) = ( ( ( * o. A ) ` k ) x. ( z ^ k ) ) )
47 46 sumeq2dv 
 |-  ( ( F e. ( Poly ` S ) /\ z e. CC ) -> sum_ k e. ( 0 ... N ) ( * ` ( ( A ` k ) x. ( ( * ` z ) ^ k ) ) ) = sum_ k e. ( 0 ... N ) ( ( ( * o. A ) ` k ) x. ( z ^ k ) ) )
48 35 47 eqtrd 
 |-  ( ( F e. ( Poly ` S ) /\ z e. CC ) -> ( * ` sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( ( * ` z ) ^ k ) ) ) = sum_ k e. ( 0 ... N ) ( ( ( * o. A ) ` k ) x. ( z ^ k ) ) )
49 48 mpteq2dva 
 |-  ( F e. ( Poly ` S ) -> ( z e. CC |-> ( * ` sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( ( * ` z ) ^ k ) ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( * o. A ) ` k ) x. ( z ^ k ) ) ) )
50 28 49 eqtrd 
 |-  ( F e. ( Poly ` S ) -> G = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( * o. A ) ` k ) x. ( z ^ k ) ) ) )