Definition df-coe

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccoe	⊢ coeff
1		vf	⊢ 𝑓
2		cply	⊢ Poly
3		cc	⊢ ℂ
4	3 2	cfv	⊢ ( Poly ‘ ℂ )
5		va	⊢ 𝑎
6		cmap	⊢ ↑m
7		cn0	⊢ ℕ0
8	3 7 6	co	⊢ ( ℂ ↑m ℕ0 )
9		vn	⊢ 𝑛
10	5	cv	⊢ 𝑎
11		cuz	⊢ ℤ≥
12	9	cv	⊢ 𝑛
13		caddc	⊢ +
14		c1	⊢ 1
15	12 14 13	co	⊢ ( 𝑛 + 1 )
16	15 11	cfv	⊢ ( ℤ≥ ‘ ( 𝑛 + 1 ) )
17	10 16	cima	⊢ ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) )
18		cc0	⊢ 0
19	18	csn	⊢ { 0 }
20	17 19	wceq	⊢ ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 }
21	1	cv	⊢ 𝑓
22		vz	⊢ 𝑧
23		vk	⊢ 𝑘
24		cfz	⊢ ...
25	18 12 24	co	⊢ ( 0 ... 𝑛 )
26	23	cv	⊢ 𝑘
27	26 10	cfv	⊢ ( 𝑎 ‘ 𝑘 )
28		cmul	⊢ ·
29	22	cv	⊢ 𝑧
30		cexp	⊢ ↑
31	29 26 30	co	⊢ ( 𝑧 ↑ 𝑘 )
32	27 31 28	co	⊢ ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) )
33	25 32 23	csu	⊢ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) )
34	22 3 33	cmpt	⊢ ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
35	21 34	wceq	⊢ 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
36	20 35	wa	⊢ ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
37	36 9 7	wrex	⊢ ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
38	37 5 8	crio	⊢ ( ℩ 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
39	1 4 38	cmpt	⊢ ( 𝑓 ∈ ( Poly ‘ ℂ ) ↦ ( ℩ 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )
40	0 39	wceq	⊢ coeff = ( 𝑓 ∈ ( Poly ‘ ℂ ) ↦ ( ℩ 𝑎 ∈ ( ℂ ↑m ℕ0 ) ∃ 𝑛 ∈ ℕ0 ( ( 𝑎 “ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) = { 0 } ∧ 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )