# Metamath Proof Explorer

## Theorem plycjlem

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

Ref Expression
Hypotheses plycj.1 ${⊢}{N}=\mathrm{deg}\left({F}\right)$
plycj.2 ${⊢}{G}=\left(*\circ {F}\right)\circ *$
plycjlem.3 ${⊢}{A}=\mathrm{coeff}\left({F}\right)$
Assertion plycjlem ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to {G}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(*\circ {A}\right)\left({k}\right){{z}}^{{k}}\right)$

### Proof

Step Hyp Ref Expression
1 plycj.1 ${⊢}{N}=\mathrm{deg}\left({F}\right)$
2 plycj.2 ${⊢}{G}=\left(*\circ {F}\right)\circ *$
3 plycjlem.3 ${⊢}{A}=\mathrm{coeff}\left({F}\right)$
4 cjcl ${⊢}{z}\in ℂ\to \stackrel{‾}{{z}}\in ℂ$
5 4 adantl ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {z}\in ℂ\right)\to \stackrel{‾}{{z}}\in ℂ$
6 cjf ${⊢}*:ℂ⟶ℂ$
7 6 a1i ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to *:ℂ⟶ℂ$
8 7 feqmptd ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to *=\left({z}\in ℂ⟼\stackrel{‾}{{z}}\right)$
9 fzfid ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {x}\in ℂ\right)\to \left(0\dots {N}\right)\in \mathrm{Fin}$
10 3 coef3 ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to {A}:{ℕ}_{0}⟶ℂ$
11 10 adantr ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {x}\in ℂ\right)\to {A}:{ℕ}_{0}⟶ℂ$
12 elfznn0 ${⊢}{k}\in \left(0\dots {N}\right)\to {k}\in {ℕ}_{0}$
13 ffvelrn ${⊢}\left({A}:{ℕ}_{0}⟶ℂ\wedge {k}\in {ℕ}_{0}\right)\to {A}\left({k}\right)\in ℂ$
14 11 12 13 syl2an ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {x}\in ℂ\right)\wedge {k}\in \left(0\dots {N}\right)\right)\to {A}\left({k}\right)\in ℂ$
15 expcl ${⊢}\left({x}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {{x}}^{{k}}\in ℂ$
16 12 15 sylan2 ${⊢}\left({x}\in ℂ\wedge {k}\in \left(0\dots {N}\right)\right)\to {{x}}^{{k}}\in ℂ$
17 16 adantll ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {x}\in ℂ\right)\wedge {k}\in \left(0\dots {N}\right)\right)\to {{x}}^{{k}}\in ℂ$
18 14 17 mulcld ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {x}\in ℂ\right)\wedge {k}\in \left(0\dots {N}\right)\right)\to {A}\left({k}\right){{x}}^{{k}}\in ℂ$
19 9 18 fsumcl ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {x}\in ℂ\right)\to \sum _{{k}=0}^{{N}}{A}\left({k}\right){{x}}^{{k}}\in ℂ$
20 3 1 coeid ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to {F}=\left({x}\in ℂ⟼\sum _{{k}=0}^{{N}}{A}\left({k}\right){{x}}^{{k}}\right)$
21 fveq2 ${⊢}{z}=\sum _{{k}=0}^{{N}}{A}\left({k}\right){{x}}^{{k}}\to \stackrel{‾}{{z}}=\stackrel{‾}{\sum _{{k}=0}^{{N}}{A}\left({k}\right){{x}}^{{k}}}$
22 19 20 8 21 fmptco ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to *\circ {F}=\left({x}\in ℂ⟼\stackrel{‾}{\sum _{{k}=0}^{{N}}{A}\left({k}\right){{x}}^{{k}}}\right)$
23 oveq1 ${⊢}{x}=\stackrel{‾}{{z}}\to {{x}}^{{k}}={\stackrel{‾}{{z}}}^{{k}}$
24 23 oveq2d ${⊢}{x}=\stackrel{‾}{{z}}\to {A}\left({k}\right){{x}}^{{k}}={A}\left({k}\right){\stackrel{‾}{{z}}}^{{k}}$
25 24 sumeq2sdv ${⊢}{x}=\stackrel{‾}{{z}}\to \sum _{{k}=0}^{{N}}{A}\left({k}\right){{x}}^{{k}}=\sum _{{k}=0}^{{N}}{A}\left({k}\right){\stackrel{‾}{{z}}}^{{k}}$
26 25 fveq2d ${⊢}{x}=\stackrel{‾}{{z}}\to \stackrel{‾}{\sum _{{k}=0}^{{N}}{A}\left({k}\right){{x}}^{{k}}}=\stackrel{‾}{\sum _{{k}=0}^{{N}}{A}\left({k}\right){\stackrel{‾}{{z}}}^{{k}}}$
27 5 8 22 26 fmptco ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to \left(*\circ {F}\right)\circ *=\left({z}\in ℂ⟼\stackrel{‾}{\sum _{{k}=0}^{{N}}{A}\left({k}\right){\stackrel{‾}{{z}}}^{{k}}}\right)$
28 2 27 syl5eq ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to {G}=\left({z}\in ℂ⟼\stackrel{‾}{\sum _{{k}=0}^{{N}}{A}\left({k}\right){\stackrel{‾}{{z}}}^{{k}}}\right)$
29 fzfid ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {z}\in ℂ\right)\to \left(0\dots {N}\right)\in \mathrm{Fin}$
30 10 adantr ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {z}\in ℂ\right)\to {A}:{ℕ}_{0}⟶ℂ$
31 30 12 13 syl2an ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {z}\in ℂ\right)\wedge {k}\in \left(0\dots {N}\right)\right)\to {A}\left({k}\right)\in ℂ$
32 expcl ${⊢}\left(\stackrel{‾}{{z}}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {\stackrel{‾}{{z}}}^{{k}}\in ℂ$
33 5 12 32 syl2an ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {z}\in ℂ\right)\wedge {k}\in \left(0\dots {N}\right)\right)\to {\stackrel{‾}{{z}}}^{{k}}\in ℂ$
34 31 33 mulcld ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {z}\in ℂ\right)\wedge {k}\in \left(0\dots {N}\right)\right)\to {A}\left({k}\right){\stackrel{‾}{{z}}}^{{k}}\in ℂ$
35 29 34 fsumcj ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {z}\in ℂ\right)\to \stackrel{‾}{\sum _{{k}=0}^{{N}}{A}\left({k}\right){\stackrel{‾}{{z}}}^{{k}}}=\sum _{{k}=0}^{{N}}\stackrel{‾}{{A}\left({k}\right){\stackrel{‾}{{z}}}^{{k}}}$
36 31 33 cjmuld ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {z}\in ℂ\right)\wedge {k}\in \left(0\dots {N}\right)\right)\to \stackrel{‾}{{A}\left({k}\right){\stackrel{‾}{{z}}}^{{k}}}=\stackrel{‾}{{A}\left({k}\right)}\stackrel{‾}{{\stackrel{‾}{{z}}}^{{k}}}$
37 fvco3 ${⊢}\left({A}:{ℕ}_{0}⟶ℂ\wedge {k}\in {ℕ}_{0}\right)\to \left(*\circ {A}\right)\left({k}\right)=\stackrel{‾}{{A}\left({k}\right)}$
38 30 12 37 syl2an ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {z}\in ℂ\right)\wedge {k}\in \left(0\dots {N}\right)\right)\to \left(*\circ {A}\right)\left({k}\right)=\stackrel{‾}{{A}\left({k}\right)}$
39 cjexp ${⊢}\left(\stackrel{‾}{{z}}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to \stackrel{‾}{{\stackrel{‾}{{z}}}^{{k}}}={\stackrel{‾}{\stackrel{‾}{{z}}}}^{{k}}$
40 5 12 39 syl2an ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {z}\in ℂ\right)\wedge {k}\in \left(0\dots {N}\right)\right)\to \stackrel{‾}{{\stackrel{‾}{{z}}}^{{k}}}={\stackrel{‾}{\stackrel{‾}{{z}}}}^{{k}}$
41 cjcj ${⊢}{z}\in ℂ\to \stackrel{‾}{\stackrel{‾}{{z}}}={z}$
42 41 ad2antlr ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {z}\in ℂ\right)\wedge {k}\in \left(0\dots {N}\right)\right)\to \stackrel{‾}{\stackrel{‾}{{z}}}={z}$
43 42 oveq1d ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {z}\in ℂ\right)\wedge {k}\in \left(0\dots {N}\right)\right)\to {\stackrel{‾}{\stackrel{‾}{{z}}}}^{{k}}={{z}}^{{k}}$
44 40 43 eqtr2d ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {z}\in ℂ\right)\wedge {k}\in \left(0\dots {N}\right)\right)\to {{z}}^{{k}}=\stackrel{‾}{{\stackrel{‾}{{z}}}^{{k}}}$
45 38 44 oveq12d ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {z}\in ℂ\right)\wedge {k}\in \left(0\dots {N}\right)\right)\to \left(*\circ {A}\right)\left({k}\right){{z}}^{{k}}=\stackrel{‾}{{A}\left({k}\right)}\stackrel{‾}{{\stackrel{‾}{{z}}}^{{k}}}$
46 36 45 eqtr4d ${⊢}\left(\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {z}\in ℂ\right)\wedge {k}\in \left(0\dots {N}\right)\right)\to \stackrel{‾}{{A}\left({k}\right){\stackrel{‾}{{z}}}^{{k}}}=\left(*\circ {A}\right)\left({k}\right){{z}}^{{k}}$
47 46 sumeq2dv ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {z}\in ℂ\right)\to \sum _{{k}=0}^{{N}}\stackrel{‾}{{A}\left({k}\right){\stackrel{‾}{{z}}}^{{k}}}=\sum _{{k}=0}^{{N}}\left(*\circ {A}\right)\left({k}\right){{z}}^{{k}}$
48 35 47 eqtrd ${⊢}\left({F}\in \mathrm{Poly}\left({S}\right)\wedge {z}\in ℂ\right)\to \stackrel{‾}{\sum _{{k}=0}^{{N}}{A}\left({k}\right){\stackrel{‾}{{z}}}^{{k}}}=\sum _{{k}=0}^{{N}}\left(*\circ {A}\right)\left({k}\right){{z}}^{{k}}$
49 48 mpteq2dva ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to \left({z}\in ℂ⟼\stackrel{‾}{\sum _{{k}=0}^{{N}}{A}\left({k}\right){\stackrel{‾}{{z}}}^{{k}}}\right)=\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(*\circ {A}\right)\left({k}\right){{z}}^{{k}}\right)$
50 28 49 eqtrd ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to {G}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}\left(*\circ {A}\right)\left({k}\right){{z}}^{{k}}\right)$