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

Definition df-ply 24235
Description: Define the set of polynomials on the complex numbers with coefficients in the given subset. (Contributed by Mario Carneiro, 17-Jul-2014.)
Assertion
Ref Expression
df-ply Poly = (𝑥 ∈ 𝒫 ℂ ↦ {𝑓 ∣ ∃𝑛 ∈ ℕ0𝑎 ∈ ((𝑥 ∪ {0}) ↑𝑚0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))})
Distinct variable group:   𝑓,𝑎,𝑘,𝑛,𝑥,𝑧

Detailed syntax breakdown of Definition df-ply
StepHypRef Expression
1 cply 24231 . 2 class Poly
2 vx . . 3 setvar 𝑥
3 cc 10187 . . . 4 class
43cpw 4315 . . 3 class 𝒫 ℂ
5 vf . . . . . . . 8 setvar 𝑓
65cv 1651 . . . . . . 7 class 𝑓
7 vz . . . . . . . 8 setvar 𝑧
8 cc0 10189 . . . . . . . . . 10 class 0
9 vn . . . . . . . . . . 11 setvar 𝑛
109cv 1651 . . . . . . . . . 10 class 𝑛
11 cfz 12533 . . . . . . . . . 10 class ...
128, 10, 11co 6842 . . . . . . . . 9 class (0...𝑛)
13 vk . . . . . . . . . . . 12 setvar 𝑘
1413cv 1651 . . . . . . . . . . 11 class 𝑘
15 va . . . . . . . . . . . 12 setvar 𝑎
1615cv 1651 . . . . . . . . . . 11 class 𝑎
1714, 16cfv 6068 . . . . . . . . . 10 class (𝑎𝑘)
187cv 1651 . . . . . . . . . . 11 class 𝑧
19 cexp 13067 . . . . . . . . . . 11 class
2018, 14, 19co 6842 . . . . . . . . . 10 class (𝑧𝑘)
21 cmul 10194 . . . . . . . . . 10 class ·
2217, 20, 21co 6842 . . . . . . . . 9 class ((𝑎𝑘) · (𝑧𝑘))
2312, 22, 13csu 14701 . . . . . . . 8 class Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘))
247, 3, 23cmpt 4888 . . . . . . 7 class (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))
256, 24wceq 1652 . . . . . 6 wff 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))
262cv 1651 . . . . . . . 8 class 𝑥
278csn 4334 . . . . . . . 8 class {0}
2826, 27cun 3730 . . . . . . 7 class (𝑥 ∪ {0})
29 cn0 11538 . . . . . . 7 class 0
30 cmap 8060 . . . . . . 7 class 𝑚
3128, 29, 30co 6842 . . . . . 6 class ((𝑥 ∪ {0}) ↑𝑚0)
3225, 15, 31wrex 3056 . . . . 5 wff 𝑎 ∈ ((𝑥 ∪ {0}) ↑𝑚0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))
3332, 9, 29wrex 3056 . . . 4 wff 𝑛 ∈ ℕ0𝑎 ∈ ((𝑥 ∪ {0}) ↑𝑚0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))
3433, 5cab 2751 . . 3 class {𝑓 ∣ ∃𝑛 ∈ ℕ0𝑎 ∈ ((𝑥 ∪ {0}) ↑𝑚0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))}
352, 4, 34cmpt 4888 . 2 class (𝑥 ∈ 𝒫 ℂ ↦ {𝑓 ∣ ∃𝑛 ∈ ℕ0𝑎 ∈ ((𝑥 ∪ {0}) ↑𝑚0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))})
361, 35wceq 1652 1 wff Poly = (𝑥 ∈ 𝒫 ℂ ↦ {𝑓 ∣ ∃𝑛 ∈ ℕ0𝑎 ∈ ((𝑥 ∪ {0}) ↑𝑚0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎𝑘) · (𝑧𝑘)))})
Colors of variables: wff setvar class
This definition is referenced by:  plyval  24240  plybss  24241
  Copyright terms: Public domain W3C validator