Definition df-ply 25926

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 25922	. 2 class Poly
2		vx	. . 3 setvar 𝑥
3		cc 11110	. . . 4 class ℂ
4	3	cpw 4602	. . 3 class 𝒫 ℂ
5		vf	. . . . . . . 8 setvar 𝑓
6	5	cv 1540	. . . . . . 7 class 𝑓
7		vz	. . . . . . . 8 setvar 𝑧
8		cc0 11112	. . . . . . . . . 10 class 0
9		vn	. . . . . . . . . . 11 setvar 𝑛
10	9	cv 1540	. . . . . . . . . 10 class 𝑛
11		cfz 13488	. . . . . . . . . 10 class ...
12	8, 10, 11	co 7411	. . . . . . . . 9 class (0...𝑛)
13		vk	. . . . . . . . . . . 12 setvar 𝑘
14	13	cv 1540	. . . . . . . . . . 11 class 𝑘
15		va	. . . . . . . . . . . 12 setvar 𝑎
16	15	cv 1540	. . . . . . . . . . 11 class 𝑎
17	14, 16	cfv 6543	. . . . . . . . . 10 class (𝑎‘𝑘)
18	7	cv 1540	. . . . . . . . . . 11 class 𝑧
19		cexp 14031	. . . . . . . . . . 11 class ↑
20	18, 14, 19	co 7411	. . . . . . . . . 10 class (𝑧↑𝑘)
21		cmul 11117	. . . . . . . . . 10 class ·
22	17, 20, 21	co 7411	. . . . . . . . 9 class ((𝑎‘𝑘) · (𝑧↑𝑘))
23	12, 22, 13	csu 15636	. . . . . . . 8 class Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))
24	7, 3, 23	cmpt 5231	. . . . . . 7 class (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))
25	6, 24	wceq 1541	. . . . . 6 wff 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))
26	2	cv 1540	. . . . . . . 8 class 𝑥
27	8	csn 4628	. . . . . . . 8 class {0}
28	26, 27	cun 3946	. . . . . . 7 class (𝑥 ∪ {0})
29		cn0 12476	. . . . . . 7 class ℕ0
30		cmap 8822	. . . . . . 7 class ↑m
31	28, 29, 30	co 7411	. . . . . 6 class ((𝑥 ∪ {0}) ↑m ℕ0)
32	25, 15, 31	wrex 3070	. . . . 5 wff ∃𝑎 ∈ ((𝑥 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))
33	32, 9, 29	wrex 3070	. . . 4 wff ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑥 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))
34	33, 5	cab 2709	. . 3 class {𝑓 ∣ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑥 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))}
35	2, 4, 34	cmpt 5231	. 2 class (𝑥 ∈ 𝒫 ℂ ↦ {𝑓 ∣ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑥 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))})
36	1, 35	wceq 1541	1 wff Poly = (𝑥 ∈ 𝒫 ℂ ↦ {𝑓 ∣ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((𝑥 ∪ {0}) ↑m ℕ0)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))})

This definition is referenced by:  plyval  25931  plybss  25932