Definition df-ply

Description: Define the set of polynomials on the complex numbers with coefficients in the given subset. (Contributed by Mario Carneiro, 17-Jul-2014)

	Ref	Expression
Assertion	df-ply	$$⊢\mathrm{Poly}=\left(x\in 𝒫ℂ⟼\left\{f|\exists n\in {\mathbb{N}}_0\exists a\in \left({\left(x\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cply	$$class\mathrm{Poly}$$
1		vx	$$setvarx$$
2		cc	$$classℂ$$
3	2	cpw	$$class𝒫ℂ$$
4		vf	$$setvarf$$
5		vn	$$setvarn$$
6		cn0	$$class{\mathbb{N}}_0$$
7		va	$$setvara$$
8	1	cv	$$setvarx$$
9		cc0	$$class0$$
10	9	csn	$$class\left\{0\right\}$$
11	8 10	cun	$$class\left(x\cup \left\{0\right\}\right)$$
12		cmap	$$class{\uparrow }_{𝑚}$$
13	11 6 12	co	$$class\left({\left(x\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)$$
14	4	cv	$$setvarf$$
15		vz	$$setvarz$$
16		vk	$$setvark$$
17		cfz	$$class\dots$$
18	5	cv	$$setvarn$$
19	9 18 17	co	$$class\left(0\dots n\right)$$
20	7	cv	$$setvara$$
21	16	cv	$$setvark$$
22	21 20	cfv	$$classa\left(k\right)$$
23		cmul	$$class\times$$
24	15	cv	$$setvarz$$
25		cexp	$$class^$$
26	24 21 25	co	$$class{z}^k$$
27	22 26 23	co	$$classa\left(k\right)z^k$$
28	19 27 16	csu	$$class\sum _{k=0}^{n}a\left(k\right)z^k$$
29	15 2 28	cmpt	$$class\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)$$
30	14 29	wceq	$$wfff=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)$$
31	30 7 13	wrex	$$wff\exists a\in \left({\left(x\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)$$
32	31 5 6	wrex	$$wff\exists n\in {\mathbb{N}}_0\exists a\in \left({\left(x\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)$$
33	32 4	cab	$$class\left\{f|\exists n\in {\mathbb{N}}_0\exists a\in \left({\left(x\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right\}$$
34	1 3 33	cmpt	$$class\left(x\in 𝒫ℂ⟼\left\{f|\exists n\in {\mathbb{N}}_0\exists a\in \left({\left(x\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right\}\right)$$
35	0 34	wceq	$$wff\mathrm{Poly}=\left(x\in 𝒫ℂ⟼\left\{f|\exists n\in {\mathbb{N}}_0\exists a\in \left({\left(x\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right\}\right)$$