This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) ) )