Definition df-ply 25702

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 25698	. 2 class Poly
2		vx	. . 3 setvar 𝑥
3		cc 11108	. . . 4 class ℂ
4	3	cpw 4603	. . 3 class 𝒫 ℂ
5		vf	. . . . . . . 8 setvar 𝑓
6	5	cv 1541	. . . . . . 7 class 𝑓
7		vz	. . . . . . . 8 setvar 𝑧
8		cc0 11110	. . . . . . . . . 10 class 0
9		vn	. . . . . . . . . . 11 setvar 𝑛
10	9	cv 1541	. . . . . . . . . 10 class 𝑛
11		cfz 13484	. . . . . . . . . 10 class ...
12	8, 10, 11	co 7409	. . . . . . . . 9 class (0...𝑛)
13		vk	. . . . . . . . . . . 12 setvar 𝑘
14	13	cv 1541	. . . . . . . . . . 11 class 𝑘
15		va	. . . . . . . . . . . 12 setvar 𝑎
16	15	cv 1541	. . . . . . . . . . 11 class 𝑎
17	14, 16	cfv 6544	. . . . . . . . . 10 class (𝑎‘𝑘)
18	7	cv 1541	. . . . . . . . . . 11 class 𝑧
19		cexp 14027	. . . . . . . . . . 11 class ↑
20	18, 14, 19	co 7409	. . . . . . . . . 10 class (𝑧↑𝑘)
21		cmul 11115	. . . . . . . . . 10 class ·
22	17, 20, 21	co 7409	. . . . . . . . 9 class ((𝑎‘𝑘) · (𝑧↑𝑘))
23	12, 22, 13	csu 15632	. . . . . . . 8 class Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))
24	7, 3, 23	cmpt 5232	. . . . . . 7 class (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))
25	6, 24	wceq 1542	. . . . . 6 wff 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))
26	2	cv 1541	. . . . . . . 8 class 𝑥
27	8	csn 4629	. . . . . . . 8 class {0}
28	26, 27	cun 3947	. . . . . . 7 class (𝑥 ∪ {0})
29		cn0 12472	. . . . . . 7 class ℕ0
30		cmap 8820	. . . . . . 7 class ↑m
31	28, 29, 30	co 7409	. . . . . 6 class ((𝑥 ∪ {0}) ↑m ℕ0)
32	25, 15, 31	wrex 3071	. . . . 5 wff ∃𝑎 ∈ ((𝑥 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))
33	32, 9, 29	wrex 3071	. . . 4 wff ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑥 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))
34	33, 5	cab 2710	. . 3 class {𝑓 ∣ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑥 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))}
35	2, 4, 34	cmpt 5232	. 2 class (𝑥 ∈ 𝒫 ℂ ↦ {𝑓 ∣ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑥 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))})
36	1, 35	wceq 1542	1 wff Poly = (𝑥 ∈ 𝒫 ℂ ↦ {𝑓 ∣ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑥 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))})

This definition is referenced by:  plyval  25707  plybss  25708