Definition df-ply 15412

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

Step	Hyp	Ref	Expression
1		cply 15410	. 2 class Poly
2		vx	. . 3 setvar 𝑥
3		cc 8005	. . . 4 class ℂ
4	3	cpw 3649	. . 3 class 𝒫 ℂ
5		vf	. . . . . . . 8 setvar 𝑓
6	5	cv 1394	. . . . . . 7 class 𝑓
7		vz	. . . . . . . 8 setvar 𝑧
8		cc0 8007	. . . . . . . . . 10 class 0
9		vn	. . . . . . . . . . 11 setvar 𝑛
10	9	cv 1394	. . . . . . . . . 10 class 𝑛
11		cfz 10212	. . . . . . . . . 10 class ...
12	8, 10, 11	co 6007	. . . . . . . . 9 class (0...𝑛)
13		vk	. . . . . . . . . . . 12 setvar 𝑘
14	13	cv 1394	. . . . . . . . . . 11 class 𝑘
15		va	. . . . . . . . . . . 12 setvar 𝑎
16	15	cv 1394	. . . . . . . . . . 11 class 𝑎
17	14, 16	cfv 5318	. . . . . . . . . 10 class (𝑎‘𝑘)
18	7	cv 1394	. . . . . . . . . . 11 class 𝑧
19		cexp 10768	. . . . . . . . . . 11 class ↑
20	18, 14, 19	co 6007	. . . . . . . . . 10 class (𝑧↑𝑘)
21		cmul 8012	. . . . . . . . . 10 class ·
22	17, 20, 21	co 6007	. . . . . . . . 9 class ((𝑎‘𝑘) · (𝑧↑𝑘))
23	12, 22, 13	csu 11872	. . . . . . . 8 class Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))
24	7, 3, 23	cmpt 4145	. . . . . . 7 class (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))
25	6, 24	wceq 1395	. . . . . 6 wff 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))
26	2	cv 1394	. . . . . . . 8 class 𝑥
27	8	csn 3666	. . . . . . . 8 class {0}
28	26, 27	cun 3195	. . . . . . 7 class (𝑥 ∪ {0})
29		cn0 9377	. . . . . . 7 class ℕ0
30		cmap 6803	. . . . . . 7 class ↑𝑚
31	28, 29, 30	co 6007	. . . . . 6 class ((𝑥 ∪ {0}) ↑𝑚 ℕ0)
32	25, 15, 31	wrex 2509	. . . . 5 wff ∃𝑎 ∈ ((𝑥 ∪ {0}) ↑𝑚 ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))
33	32, 9, 29	wrex 2509	. . . 4 wff ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑥 ∪ {0}) ↑𝑚 ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))
34	33, 5	cab 2215	. . 3 class {𝑓 ∣ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑥 ∪ {0}) ↑𝑚 ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))}
35	2, 4, 34	cmpt 4145	. 2 class (𝑥 ∈ 𝒫 ℂ ↦ {𝑓 ∣ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑥 ∪ {0}) ↑𝑚 ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))})
36	1, 35	wceq 1395	1 wff Poly = (𝑥 ∈ 𝒫 ℂ ↦ {𝑓 ∣ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑥 ∪ {0}) ↑𝑚 ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))})

This definition is referenced by:  plyval  15414  plybss  15415