Theorem plycjlem 26556

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

Hypotheses

Ref	Expression
plycjlem.1	⊢ 𝑁 = (deg‘𝐹)
plycjlem.2	⊢ 𝐺 = ((∗ ∘ 𝐹) ∘ ∗)
plycjlem.3	⊢ 𝐴 = (coeff‘𝐹)

Assertion

Ref	Expression
plycjlem	⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((∗ ∘ 𝐴)‘𝑘) · (𝑧↑𝑘))))

Distinct variable groups:   𝑧,𝑘,𝐴   𝑘,𝐹,𝑧   𝑘,𝑁,𝑧   𝑆,𝑘,𝑧

Allowed substitution hints:   𝐺(𝑧, 𝑘)

Proof of Theorem plycjlem

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		plycjlem.2	. . 3 ⊢ 𝐺 = ((∗ ∘ 𝐹) ∘ ∗)
2		cjcl 15239	. . . . 5 ⊢ (𝑧 ∈ ℂ → (∗‘𝑧) ∈ ℂ)
3	2	adantl 487	. . . 4 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) → (∗‘𝑧) ∈ ℂ)
4		cjf 15238	. . . . . 6 ⊢ ∗:ℂ⟶ℂ
5	4	a1i 11	. . . . 5 ⊢ (𝐹 ∈ (Poly‘𝑆) → ∗:ℂ⟶ℂ)
6	5	feqmptd 6941	. . . 4 ⊢ (𝐹 ∈ (Poly‘𝑆) → ∗ = (𝑧 ∈ ℂ ↦ (∗‘𝑧)))
7		fzfid 14084	. . . . . 6 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑥 ∈ ℂ) → (0...𝑁) ∈ Fin)
8		plycjlem.3	. . . . . . . . . 10 ⊢ 𝐴 = (coeff‘𝐹)
9	8	coef3 26512	. . . . . . . . 9 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ)
10	9	adantr 486	. . . . . . . 8 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑥 ∈ ℂ) → 𝐴:ℕ0⟶ℂ)
11		elfznn0 13722	. . . . . . . 8 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
12		ffvelcdm 7069	. . . . . . . 8 ⊢ ((𝐴:ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ)
13	10, 11, 12	syl2an 608	. . . . . . 7 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ)
14		expcl 14190	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑥↑𝑘) ∈ ℂ)
15	11, 14	sylan2 605	. . . . . . . 8 ⊢ ((𝑥 ∈ ℂ ∧ 𝑘 ∈ (0...𝑁)) → (𝑥↑𝑘) ∈ ℂ)
16	15	adantll 727	. . . . . . 7 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥↑𝑘) ∈ ℂ)
17	13, 16	mulcld 11300	. . . . . 6 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ ℂ)
18	7, 17	fsumcl 15866	. . . . 5 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑥 ∈ ℂ) → Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ ℂ)
19		plycjlem.1	. . . . . 6 ⊢ 𝑁 = (deg‘𝐹)
20	8, 19	coeid 26518	. . . . 5 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹 = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑥↑𝑘))))
21		fveq2 6873	. . . . 5 ⊢ (𝑧 = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑥↑𝑘)) → (∗‘𝑧) = (∗‘Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑥↑𝑘))))
22	18, 20, 6, 21	fmptco 7118	. . . 4 ⊢ (𝐹 ∈ (Poly‘𝑆) → (∗ ∘ 𝐹) = (𝑥 ∈ ℂ ↦ (∗‘Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑥↑𝑘)))))
23		oveq1 7415	. . . . . . 7 ⊢ (𝑥 = (∗‘𝑧) → (𝑥↑𝑘) = ((∗‘𝑧)↑𝑘))
24	23	oveq2d 7424	. . . . . 6 ⊢ (𝑥 = (∗‘𝑧) → ((𝐴‘𝑘) · (𝑥↑𝑘)) = ((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘)))
25	24	sumeq2sdv 15837	. . . . 5 ⊢ (𝑥 = (∗‘𝑧) → Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑥↑𝑘)) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘)))
26	25	fveq2d 6877	. . . 4 ⊢ (𝑥 = (∗‘𝑧) → (∗‘Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑥↑𝑘))) = (∗‘Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘))))
27	3, 6, 22, 26	fmptco 7118	. . 3 ⊢ (𝐹 ∈ (Poly‘𝑆) → ((∗ ∘ 𝐹) ∘ ∗) = (𝑧 ∈ ℂ ↦ (∗‘Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘)))))
28	1, 27	eqtrid 2807	. 2 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐺 = (𝑧 ∈ ℂ ↦ (∗‘Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘)))))
29		fzfid 14084	. . . . 5 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) → (0...𝑁) ∈ Fin)
30	9	adantr 486	. . . . . . 7 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) → 𝐴:ℕ0⟶ℂ)
31	30, 11, 12	syl2an 608	. . . . . 6 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ)
32		expcl 14190	. . . . . . 7 ⊢ (((∗‘𝑧) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((∗‘𝑧)↑𝑘) ∈ ℂ)
33	3, 11, 32	syl2an 608	. . . . . 6 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → ((∗‘𝑧)↑𝑘) ∈ ℂ)
34	31, 33	mulcld 11300	. . . . 5 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘)) ∈ ℂ)
35	29, 34	fsumcj 15944	. . . 4 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) → (∗‘Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘))) = Σ𝑘 ∈ (0...𝑁)(∗‘((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘))))
36	31, 33	cjmuld 15355	. . . . . 6 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (∗‘((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘))) = ((∗‘(𝐴‘𝑘)) · (∗‘((∗‘𝑧)↑𝑘))))
37		fvco3 6973	. . . . . . . 8 ⊢ ((𝐴:ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → ((∗ ∘ 𝐴)‘𝑘) = (∗‘(𝐴‘𝑘)))
38	30, 11, 37	syl2an 608	. . . . . . 7 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → ((∗ ∘ 𝐴)‘𝑘) = (∗‘(𝐴‘𝑘)))
39		cjexp 15284	. . . . . . . . 9 ⊢ (((∗‘𝑧) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (∗‘((∗‘𝑧)↑𝑘)) = ((∗‘(∗‘𝑧))↑𝑘))
40	3, 11, 39	syl2an 608	. . . . . . . 8 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (∗‘((∗‘𝑧)↑𝑘)) = ((∗‘(∗‘𝑧))↑𝑘))
41		cjcj 15274	. . . . . . . . . 10 ⊢ (𝑧 ∈ ℂ → (∗‘(∗‘𝑧)) = 𝑧)
42	41	ad2antlr 740	. . . . . . . . 9 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (∗‘(∗‘𝑧)) = 𝑧)
43	42	oveq1d 7423	. . . . . . . 8 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → ((∗‘(∗‘𝑧))↑𝑘) = (𝑧↑𝑘))
44	40, 43	eqtr2d 2796	. . . . . . 7 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑧↑𝑘) = (∗‘((∗‘𝑧)↑𝑘)))
45	38, 44	oveq12d 7426	. . . . . 6 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (((∗ ∘ 𝐴)‘𝑘) · (𝑧↑𝑘)) = ((∗‘(𝐴‘𝑘)) · (∗‘((∗‘𝑧)↑𝑘))))
46	36, 45	eqtr4d 2798	. . . . 5 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (∗‘((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘))) = (((∗ ∘ 𝐴)‘𝑘) · (𝑧↑𝑘)))
47	46	sumeq2dv 15836	. . . 4 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑁)(∗‘((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘))) = Σ𝑘 ∈ (0...𝑁)(((∗ ∘ 𝐴)‘𝑘) · (𝑧↑𝑘)))
48	35, 47	eqtrd 2795	. . 3 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) → (∗‘Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘))) = Σ𝑘 ∈ (0...𝑁)(((∗ ∘ 𝐴)‘𝑘) · (𝑧↑𝑘)))
49	48	mpteq2dva 5197	. 2 ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝑧 ∈ ℂ ↦ (∗‘Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘)))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((∗ ∘ 𝐴)‘𝑘) · (𝑧↑𝑘))))
50	28, 49	eqtrd 2795	1 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((∗ ∘ 𝐴)‘𝑘) · (𝑧↑𝑘))))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ↦ cmpt 5185   ∘ ccom 5651  ⟶wf 6523  ‘cfv 6527  (class class class)co 7408  ℂcc 11169  0cc0 11171   · cmul 11176  ℕ₀cn0 12575  ...cfz 13608  ↑cexp 14172  ∗ccj 15230  Σcsu 15820  Polycply 26463  coeffccoe 26465  degcdgr 26466

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7734  ax-inf2 9620  ax-cnex 11227  ax-resscn 11228  ax-1cn 11229  ax-icn 11230  ax-addcl 11231  ax-addrcl 11232  ax-mulcl 11233  ax-mulrcl 11234  ax-mulcom 11235  ax-addass 11236  ax-mulass 11237  ax-distr 11238  ax-i2m1 11239  ax-1ne0 11240  ax-1rid 11241  ax-rnegex 11242  ax-rrecex 11243  ax-cnre 11244  ax-pre-lttri 11245  ax-pre-lttrn 11246  ax-pre-ltadd 11247  ax-pre-mulgt0 11248  ax-pre-sup 11249

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-se 5601  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6293  df-ord 6354  df-on 6355  df-lim 6356  df-suc 6357  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-isom 6536  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-of 7676  df-om 7861  df-1st 7984  df-2nd 7985  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-1o 8454  df-er 8695  df-map 8827  df-pm 8828  df-en 8952  df-dom 8953  df-sdom 8954  df-fin 8955  df-sup 9412  df-inf 9413  df-oi 9482  df-card 9991  df-pnf 11316  df-mnf 11317  df-xr 11318  df-ltxr 11319  df-le 11320  df-sub 11514  df-neg 11515  df-div 11943  df-nn 12305  df-2 12374  df-3 12375  df-n0 12576  df-z 12663  df-uz 12935  df-rp 13090  df-fz 13609  df-fzo 13757  df-fl 13900  df-seq 14113  df-exp 14173  df-hash 14442  df-cj 15233  df-re 15234  df-im 15235  df-sqrt 15369  df-abs 15370  df-clim 15622  df-rlim 15623  df-sum 15821  df-0p 25952  df-ply 26467  df-coe 26469  df-dgr 26470

This theorem is used by:  plycj  26557  coecj  26558  plycjOLD  26559  coecjOLD  26560