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 ... 𝑁 ) ( ( ( ∗ ∘ 𝐴 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )