# Metamath Proof Explorer

## Theorem plycjlem

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

Ref Expression
Hypotheses plycj.1
`|- N = ( deg ` F )`
plycj.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 plycj.1
` |-  N = ( deg ` F )`
2 plycj.2
` |-  G = ( ( * o. F ) o. * )`
3 plycjlem.3
` |-  A = ( coeff ` F )`
4 cjcl
` |-  ( z e. CC -> ( * ` z ) e. CC )`
` |-  ( ( 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 )`
` |-  ( ( F e. ( Poly ` S ) /\ x e. CC ) -> A : NN0 --> CC )`
12 elfznn0
` |-  ( k e. ( 0 ... N ) -> k e. NN0 )`
13 ffvelrn
` |-  ( ( 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 )`
` |-  ( ( ( 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 syl5eq
` |-  ( 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 )`
` |-  ( ( 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 )`
` |-  ( ( ( 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 ) ) ) )`