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

Definition df-coe 23664
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 23660 . 2 class coeff
2 vf . . 3 setvar 𝑓
3 cc 9787 . . . 4 class
4 cply 23658 . . . 4 class Poly
53, 4cfv 5787 . . 3 class (Poly‘ℂ)
6 va . . . . . . . . 9 setvar 𝑎
76cv 1473 . . . . . . . 8 class 𝑎
8 vn . . . . . . . . . . 11 setvar 𝑛
98cv 1473 . . . . . . . . . 10 class 𝑛
10 c1 9790 . . . . . . . . . 10 class 1
11 caddc 9792 . . . . . . . . . 10 class +
129, 10, 11co 6524 . . . . . . . . 9 class (𝑛 + 1)
13 cuz 11516 . . . . . . . . 9 class
1412, 13cfv 5787 . . . . . . . 8 class (ℤ‘(𝑛 + 1))
157, 14cima 5028 . . . . . . 7 class (𝑎 “ (ℤ‘(𝑛 + 1)))
16 cc0 9789 . . . . . . . 8 class 0
1716csn 4121 . . . . . . 7 class {0}
1815, 17wceq 1474 . . . . . 6 wff (𝑎 “ (ℤ‘(𝑛 + 1))) = {0}
192cv 1473 . . . . . . 7 class 𝑓
20 vz . . . . . . . 8 setvar 𝑧
21 cfz 12149 . . . . . . . . . 10 class ...
2216, 9, 21co 6524 . . . . . . . . 9 class (0...𝑛)
23 vk . . . . . . . . . . . 12 setvar 𝑘
2423cv 1473 . . . . . . . . . . 11 class 𝑘
2524, 7cfv 5787 . . . . . . . . . 10 class (𝑎𝑘)
2620cv 1473 . . . . . . . . . . 11 class 𝑧
27 cexp 12674 . . . . . . . . . . 11 class
2826, 24, 27co 6524 . . . . . . . . . 10 class (𝑧𝑘)
29 cmul 9794 . . . . . . . . . 10 class ·
3025, 28, 29co 6524 . . . . . . . . 9 class ((𝑎𝑘) · (𝑧𝑘))
3122, 30, 23csu 14207 . . . . . . . 8 class Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))
3220, 3, 31cmpt 4634 . . . . . . 7 class (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))
3319, 32wceq 1474 . . . . . 6 wff 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))
3418, 33wa 382 . . . . 5 wff ((𝑎 “ (ℤ‘(𝑛 + 1))) = {0} ∧ 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))))
35 cn0 11136 . . . . 5 class 0
3634, 8, 35wrex 2893 . . . 4 wff 𝑛 ∈ ℕ0 ((𝑎 “ (ℤ‘(𝑛 + 1))) = {0} ∧ 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))))
37 cmap 7718 . . . . 5 class 𝑚
383, 35, 37co 6524 . . . 4 class (ℂ ↑𝑚0)
3936, 6, 38crio 6485 . . 3 class (𝑎 ∈ (ℂ ↑𝑚0)∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ‘(𝑛 + 1))) = {0} ∧ 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))))
402, 5, 39cmpt 4634 . 2 class (𝑓 ∈ (Poly‘ℂ) ↦ (𝑎 ∈ (ℂ ↑𝑚0)∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ‘(𝑛 + 1))) = {0} ∧ 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))))))
411, 40wceq 1474 1 wff coeff = (𝑓 ∈ (Poly‘ℂ) ↦ (𝑎 ∈ (ℂ ↑𝑚0)∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ‘(𝑛 + 1))) = {0} ∧ 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))))))
Colors of variables: wff setvar class
This definition is referenced by:  coeval  23697
  Copyright terms: Public domain W3C validator