# Metamath Proof Explorer

## Theorem plycjlem

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

Ref Expression
Hypotheses plycj.1 𝑁 = ( deg ‘ 𝐹 )
plycj.2 𝐺 = ( ( ∗ ∘ 𝐹 ) ∘ ∗ )
plycjlem.3 𝐴 = ( coeff ‘ 𝐹 )
Assertion plycjlem ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ∗ ∘ 𝐴 ) ‘ 𝑘 ) · ( 𝑧𝑘 ) ) ) )

### Proof

Step Hyp Ref Expression
1 plycj.1 𝑁 = ( deg ‘ 𝐹 )
2 plycj.2 𝐺 = ( ( ∗ ∘ 𝐹 ) ∘ ∗ )
3 plycjlem.3 𝐴 = ( coeff ‘ 𝐹 )
4 cjcl ( 𝑧 ∈ ℂ → ( ∗ ‘ 𝑧 ) ∈ ℂ )
5 4 adantl ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑧 ∈ ℂ ) → ( ∗ ‘ 𝑧 ) ∈ ℂ )
6 cjf ∗ : ℂ ⟶ ℂ
7 6 a1i ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∗ : ℂ ⟶ ℂ )
8 7 feqmptd ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ∗ = ( 𝑧 ∈ ℂ ↦ ( ∗ ‘ 𝑧 ) ) )
9 fzfid ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑥 ∈ ℂ ) → ( 0 ... 𝑁 ) ∈ Fin )
10 3 coef3 ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
11 10 adantr ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑥 ∈ ℂ ) → 𝐴 : ℕ0 ⟶ ℂ )
12 elfznn0 ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
13 ffvelrn ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴𝑘 ) ∈ ℂ )
14 11 12 13 syl2an ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴𝑘 ) ∈ ℂ )
15 expcl ( ( 𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑥𝑘 ) ∈ ℂ )
16 12 15 sylan2 ( ( 𝑥 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑥𝑘 ) ∈ ℂ )
17 16 adantll ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑥𝑘 ) ∈ ℂ )
18 14 17 mulcld ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴𝑘 ) · ( 𝑥𝑘 ) ) ∈ ℂ )
19 9 18 fsumcl ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑥 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴𝑘 ) · ( 𝑥𝑘 ) ) ∈ ℂ )
20 3 1 coeid ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 = ( 𝑥 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴𝑘 ) · ( 𝑥𝑘 ) ) ) )
21 fveq2 ( 𝑧 = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴𝑘 ) · ( 𝑥𝑘 ) ) → ( ∗ ‘ 𝑧 ) = ( ∗ ‘ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴𝑘 ) · ( 𝑥𝑘 ) ) ) )
22 19 20 8 21 fmptco ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ∗ ∘ 𝐹 ) = ( 𝑥 ∈ ℂ ↦ ( ∗ ‘ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴𝑘 ) · ( 𝑥𝑘 ) ) ) ) )
23 oveq1 ( 𝑥 = ( ∗ ‘ 𝑧 ) → ( 𝑥𝑘 ) = ( ( ∗ ‘ 𝑧 ) ↑ 𝑘 ) )
24 23 oveq2d ( 𝑥 = ( ∗ ‘ 𝑧 ) → ( ( 𝐴𝑘 ) · ( 𝑥𝑘 ) ) = ( ( 𝐴𝑘 ) · ( ( ∗ ‘ 𝑧 ) ↑ 𝑘 ) ) )
25 24 sumeq2sdv ( 𝑥 = ( ∗ ‘ 𝑧 ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴𝑘 ) · ( 𝑥𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴𝑘 ) · ( ( ∗ ‘ 𝑧 ) ↑ 𝑘 ) ) )
26 25 fveq2d ( 𝑥 = ( ∗ ‘ 𝑧 ) → ( ∗ ‘ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴𝑘 ) · ( 𝑥𝑘 ) ) ) = ( ∗ ‘ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴𝑘 ) · ( ( ∗ ‘ 𝑧 ) ↑ 𝑘 ) ) ) )
27 5 8 22 26 fmptco ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ( ∗ ∘ 𝐹 ) ∘ ∗ ) = ( 𝑧 ∈ ℂ ↦ ( ∗ ‘ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴𝑘 ) · ( ( ∗ ‘ 𝑧 ) ↑ 𝑘 ) ) ) ) )
28 2 27 syl5eq ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐺 = ( 𝑧 ∈ ℂ ↦ ( ∗ ‘ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴𝑘 ) · ( ( ∗ ‘ 𝑧 ) ↑ 𝑘 ) ) ) ) )
29 fzfid ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑧 ∈ ℂ ) → ( 0 ... 𝑁 ) ∈ Fin )
30 10 adantr ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑧 ∈ ℂ ) → 𝐴 : ℕ0 ⟶ ℂ )
31 30 12 13 syl2an ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴𝑘 ) ∈ ℂ )
32 expcl ( ( ( ∗ ‘ 𝑧 ) ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( ∗ ‘ 𝑧 ) ↑ 𝑘 ) ∈ ℂ )
33 5 12 32 syl2an ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ∗ ‘ 𝑧 ) ↑ 𝑘 ) ∈ ℂ )
34 31 33 mulcld ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴𝑘 ) · ( ( ∗ ‘ 𝑧 ) ↑ 𝑘 ) ) ∈ ℂ )
35 29 34 fsumcj ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑧 ∈ ℂ ) → ( ∗ ‘ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴𝑘 ) · ( ( ∗ ‘ 𝑧 ) ↑ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ∗ ‘ ( ( 𝐴𝑘 ) · ( ( ∗ ‘ 𝑧 ) ↑ 𝑘 ) ) ) )
36 31 33 cjmuld ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ∗ ‘ ( ( 𝐴𝑘 ) · ( ( ∗ ‘ 𝑧 ) ↑ 𝑘 ) ) ) = ( ( ∗ ‘ ( 𝐴𝑘 ) ) · ( ∗ ‘ ( ( ∗ ‘ 𝑧 ) ↑ 𝑘 ) ) ) )
37 fvco3 ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( ∗ ∘ 𝐴 ) ‘ 𝑘 ) = ( ∗ ‘ ( 𝐴𝑘 ) ) )
38 30 12 37 syl2an ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ∗ ∘ 𝐴 ) ‘ 𝑘 ) = ( ∗ ‘ ( 𝐴𝑘 ) ) )
39 cjexp ( ( ( ∗ ‘ 𝑧 ) ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ∗ ‘ ( ( ∗ ‘ 𝑧 ) ↑ 𝑘 ) ) = ( ( ∗ ‘ ( ∗ ‘ 𝑧 ) ) ↑ 𝑘 ) )
40 5 12 39 syl2an ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ∗ ‘ ( ( ∗ ‘ 𝑧 ) ↑ 𝑘 ) ) = ( ( ∗ ‘ ( ∗ ‘ 𝑧 ) ) ↑ 𝑘 ) )
41 cjcj ( 𝑧 ∈ ℂ → ( ∗ ‘ ( ∗ ‘ 𝑧 ) ) = 𝑧 )
42 41 ad2antlr ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ∗ ‘ ( ∗ ‘ 𝑧 ) ) = 𝑧 )
43 42 oveq1d ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ∗ ‘ ( ∗ ‘ 𝑧 ) ) ↑ 𝑘 ) = ( 𝑧𝑘 ) )
44 40 43 eqtr2d ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑧𝑘 ) = ( ∗ ‘ ( ( ∗ ‘ 𝑧 ) ↑ 𝑘 ) ) )
45 38 44 oveq12d ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ∗ ∘ 𝐴 ) ‘ 𝑘 ) · ( 𝑧𝑘 ) ) = ( ( ∗ ‘ ( 𝐴𝑘 ) ) · ( ∗ ‘ ( ( ∗ ‘ 𝑧 ) ↑ 𝑘 ) ) ) )
46 36 45 eqtr4d ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ∗ ‘ ( ( 𝐴𝑘 ) · ( ( ∗ ‘ 𝑧 ) ↑ 𝑘 ) ) ) = ( ( ( ∗ ∘ 𝐴 ) ‘ 𝑘 ) · ( 𝑧𝑘 ) ) )
47 46 sumeq2dv ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ∗ ‘ ( ( 𝐴𝑘 ) · ( ( ∗ ‘ 𝑧 ) ↑ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ∗ ∘ 𝐴 ) ‘ 𝑘 ) · ( 𝑧𝑘 ) ) )
48 35 47 eqtrd ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑧 ∈ ℂ ) → ( ∗ ‘ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴𝑘 ) · ( ( ∗ ‘ 𝑧 ) ↑ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ∗ ∘ 𝐴 ) ‘ 𝑘 ) · ( 𝑧𝑘 ) ) )
49 48 mpteq2dva ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝑧 ∈ ℂ ↦ ( ∗ ‘ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴𝑘 ) · ( ( ∗ ‘ 𝑧 ) ↑ 𝑘 ) ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ∗ ∘ 𝐴 ) ‘ 𝑘 ) · ( 𝑧𝑘 ) ) ) )
50 28 49 eqtrd ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ∗ ∘ 𝐴 ) ‘ 𝑘 ) · ( 𝑧𝑘 ) ) ) )