Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-coe Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 ccoe 23746 . 2 class coeff
2 vf . . 3 setvar 𝑓
3 cc 9813 . . . 4 class
4 cply 23744 . . . 4 class Poly
53, 4cfv 5804 . . 3 class (Poly‘ℂ)
6 va . . . . . . . . 9 setvar 𝑎
76cv 1474 . . . . . . . 8 class 𝑎
8 vn . . . . . . . . . . 11 setvar 𝑛
98cv 1474 . . . . . . . . . 10 class 𝑛
10 c1 9816 . . . . . . . . . 10 class 1
11 caddc 9818 . . . . . . . . . 10 class +
129, 10, 11co 6549 . . . . . . . . 9 class (𝑛 + 1)
13 cuz 11563 . . . . . . . . 9 class
1412, 13cfv 5804 . . . . . . . 8 class (ℤ‘(𝑛 + 1))
157, 14cima 5041 . . . . . . 7 class (𝑎 “ (ℤ‘(𝑛 + 1)))
16 cc0 9815 . . . . . . . 8 class 0
1716csn 4125 . . . . . . 7 class {0}
1815, 17wceq 1475 . . . . . 6 wff (𝑎 “ (ℤ‘(𝑛 + 1))) = {0}
192cv 1474 . . . . . . 7 class 𝑓
20 vz . . . . . . . 8 setvar 𝑧
21 cfz 12197 . . . . . . . . . 10 class ...
2216, 9, 21co 6549 . . . . . . . . 9 class (0...𝑛)
23 vk . . . . . . . . . . . 12 setvar 𝑘
2423cv 1474 . . . . . . . . . . 11 class 𝑘
2524, 7cfv 5804 . . . . . . . . . 10 class (𝑎𝑘)
2620cv 1474 . . . . . . . . . . 11 class 𝑧
27 cexp 12722 . . . . . . . . . . 11 class
2826, 24, 27co 6549 . . . . . . . . . 10 class (𝑧𝑘)
29 cmul 9820 . . . . . . . . . 10 class ·
3025, 28, 29co 6549 . . . . . . . . 9 class ((𝑎𝑘) · (𝑧𝑘))
3122, 30, 23csu 14264 . . . . . . . 8 class Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))
3220, 3, 31cmpt 4643 . . . . . . 7 class (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))
3319, 32wceq 1475 . . . . . 6 wff 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))
3418, 33wa 383 . . . . 5 wff ((𝑎 “ (ℤ‘(𝑛 + 1))) = {0} ∧ 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))))
35 cn0 11169 . . . . 5 class 0
3634, 8, 35wrex 2897 . . . 4 wff 𝑛 ∈ ℕ0 ((𝑎 “ (ℤ‘(𝑛 + 1))) = {0} ∧ 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))))
37 cmap 7744 . . . . 5 class 𝑚
383, 35, 37co 6549 . . . 4 class (ℂ ↑𝑚0)
3936, 6, 38crio 6510 . . 3 class (𝑎 ∈ (ℂ ↑𝑚0)∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ‘(𝑛 + 1))) = {0} ∧ 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))))
402, 5, 39cmpt 4643 . 2 class (𝑓 ∈ (Poly‘ℂ) ↦ (𝑎 ∈ (ℂ ↑𝑚0)∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ‘(𝑛 + 1))) = {0} ∧ 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))))))
411, 40wceq 1475 1 wff coeff = (𝑓 ∈ (Poly‘ℂ) ↦ (𝑎 ∈ (ℂ ↑𝑚0)∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ‘(𝑛 + 1))) = {0} ∧ 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))))))
 Colors of variables: wff setvar class This definition is referenced by:  coeval  23783
 Copyright terms: Public domain W3C validator