Definition df-ply 24778

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}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))})

Distinct variable group:   𝑓,𝑎,𝑘,𝑛,𝑥,𝑧

Detailed syntax breakdown of Definition df-ply

Step	Hyp	Ref	Expression
1		cply 24774	. 2 class Poly
2		vx	. . 3 setvar 𝑥
3		cc 10535	. . . 4 class ℂ
4	3	cpw 4539	. . 3 class 𝒫 ℂ
5		vf	. . . . . . . 8 setvar 𝑓
6	5	cv 1536	. . . . . . 7 class 𝑓
7		vz	. . . . . . . 8 setvar 𝑧
8		cc0 10537	. . . . . . . . . 10 class 0
9		vn	. . . . . . . . . . 11 setvar 𝑛
10	9	cv 1536	. . . . . . . . . 10 class 𝑛
11		cfz 12893	. . . . . . . . . 10 class ...
12	8, 10, 11	co 7156	. . . . . . . . 9 class (0...𝑛)
13		vk	. . . . . . . . . . . 12 setvar 𝑘
14	13	cv 1536	. . . . . . . . . . 11 class 𝑘
15		va	. . . . . . . . . . . 12 setvar 𝑎
16	15	cv 1536	. . . . . . . . . . 11 class 𝑎
17	14, 16	cfv 6355	. . . . . . . . . 10 class (𝑎‘𝑘)
18	7	cv 1536	. . . . . . . . . . 11 class 𝑧
19		cexp 13430	. . . . . . . . . . 11 class ↑
20	18, 14, 19	co 7156	. . . . . . . . . 10 class (𝑧↑𝑘)
21		cmul 10542	. . . . . . . . . 10 class ·
22	17, 20, 21	co 7156	. . . . . . . . 9 class ((𝑎‘𝑘) · (𝑧↑𝑘))
23	12, 22, 13	csu 15042	. . . . . . . 8 class Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))
24	7, 3, 23	cmpt 5146	. . . . . . 7 class (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))
25	6, 24	wceq 1537	. . . . . 6 wff 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))
26	2	cv 1536	. . . . . . . 8 class 𝑥
27	8	csn 4567	. . . . . . . 8 class {0}
28	26, 27	cun 3934	. . . . . . 7 class (𝑥 ∪ {0})
29		cn0 11898	. . . . . . 7 class ℕ0
30		cmap 8406	. . . . . . 7 class ↑m
31	28, 29, 30	co 7156	. . . . . 6 class ((𝑥 ∪ {0}) ↑m ℕ0)
32	25, 15, 31	wrex 3139	. . . . 5 wff ∃𝑎 ∈ ((𝑥 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))
33	32, 9, 29	wrex 3139	. . . 4 wff ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑥 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))
34	33, 5	cab 2799	. . 3 class {𝑓 ∣ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑥 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))}
35	2, 4, 34	cmpt 5146	. 2 class (𝑥 ∈ 𝒫 ℂ ↦ {𝑓 ∣ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑥 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))})
36	1, 35	wceq 1537	1 wff Poly = (𝑥 ∈ 𝒫 ℂ ↦ {𝑓 ∣ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑥 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))})

This definition is referenced by:  plyval  24783  plybss  24784