Definition df-coe 23750

Description: Define the coefficient function for a polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.)

Assertion

Ref	Expression
df-coe	⊢ coeff = (𝑓 ∈ (Poly‘ℂ) ↦ (℩𝑎 ∈ (ℂ ↑𝑚 ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))))

Distinct variable group:   𝑓,𝑎,𝑘,𝑛,𝑧

Detailed syntax breakdown of Definition df-coe

Step	Hyp	Ref	Expression
1		ccoe 23746	. 2 class coeff
2		vf	. . 3 setvar 𝑓
3		cc 9813	. . . 4 class ℂ
4		cply 23744	. . . 4 class Poly
5	3, 4	cfv 5804	. . 3 class (Poly‘ℂ)
6		va	. . . . . . . . 9 setvar 𝑎
7	6	cv 1474	. . . . . . . 8 class 𝑎
8		vn	. . . . . . . . . . 11 setvar 𝑛
9	8	cv 1474	. . . . . . . . . 10 class 𝑛
10		c1 9816	. . . . . . . . . 10 class 1
11		caddc 9818	. . . . . . . . . 10 class +
12	9, 10, 11	co 6549	. . . . . . . . 9 class (𝑛 + 1)
13		cuz 11563	. . . . . . . . 9 class ℤ≥
14	12, 13	cfv 5804	. . . . . . . 8 class (ℤ≥‘(𝑛 + 1))
15	7, 14	cima 5041	. . . . . . 7 class (𝑎 “ (ℤ≥‘(𝑛 + 1)))
16		cc0 9815	. . . . . . . 8 class 0
17	16	csn 4125	. . . . . . 7 class {0}
18	15, 17	wceq 1475	. . . . . 6 wff (𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0}
19	2	cv 1474	. . . . . . 7 class 𝑓
20		vz	. . . . . . . 8 setvar 𝑧
21		cfz 12197	. . . . . . . . . 10 class ...
22	16, 9, 21	co 6549	. . . . . . . . 9 class (0...𝑛)
23		vk	. . . . . . . . . . . 12 setvar 𝑘
24	23	cv 1474	. . . . . . . . . . 11 class 𝑘
25	24, 7	cfv 5804	. . . . . . . . . 10 class (𝑎‘𝑘)
26	20	cv 1474	. . . . . . . . . . 11 class 𝑧
27		cexp 12722	. . . . . . . . . . 11 class ↑
28	26, 24, 27	co 6549	. . . . . . . . . 10 class (𝑧↑𝑘)
29		cmul 9820	. . . . . . . . . 10 class ·
30	25, 28, 29	co 6549	. . . . . . . . 9 class ((𝑎‘𝑘) · (𝑧↑𝑘))
31	22, 30, 23	csu 14264	. . . . . . . 8 class Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))
32	20, 3, 31	cmpt 4643	. . . . . . 7 class (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))
33	19, 32	wceq 1475	. . . . . 6 wff 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))
34	18, 33	wa 383	. . . . 5 wff ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))
35		cn0 11169	. . . . 5 class ℕ0
36	34, 8, 35	wrex 2897	. . . 4 wff ∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))
37		cmap 7744	. . . . 5 class ↑𝑚
38	3, 35, 37	co 6549	. . . 4 class (ℂ ↑𝑚 ℕ0)
39	36, 6, 38	crio 6510	. . 3 class (℩𝑎 ∈ (ℂ ↑𝑚 ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))
40	2, 5, 39	cmpt 4643	. 2 class (𝑓 ∈ (Poly‘ℂ) ↦ (℩𝑎 ∈ (ℂ ↑𝑚 ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))))
41	1, 40	wceq 1475	1 wff coeff = (𝑓 ∈ (Poly‘ℂ) ↦ (℩𝑎 ∈ (ℂ ↑𝑚 ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))))

This definition is referenced by:  coeval  23783