Definition df-ply 22348

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 = ( x e. ~P CC |-> { f | E. n e. NN0 E. a e. ( ( x u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) } )

Distinct variable group:   f, a, k, n, x, z

Detailed syntax breakdown of Definition df-ply

Step	Hyp	Ref	Expression
1		cply 22344	. 2 class Poly
2		vx	. . 3 setvar x
3		cc 9490	. . . 4 class CC
4	3	cpw 4010	. . 3 class ~P CC
5		vf	. . . . . . . 8 setvar f
6	5	cv 1378	. . . . . . 7 class f
7		vz	. . . . . . . 8 setvar z
8		cc0 9492	. . . . . . . . . 10 class 0
9		vn	. . . . . . . . . . 11 setvar n
10	9	cv 1378	. . . . . . . . . 10 class n
11		cfz 11672	. . . . . . . . . 10 class ...
12	8, 10, 11	co 6284	. . . . . . . . 9 class ( 0 ... n )
13		vk	. . . . . . . . . . . 12 setvar k
14	13	cv 1378	. . . . . . . . . . 11 class k
15		va	. . . . . . . . . . . 12 setvar a
16	15	cv 1378	. . . . . . . . . . 11 class a
17	14, 16	cfv 5588	. . . . . . . . . 10 class ( a ` k )
18	7	cv 1378	. . . . . . . . . . 11 class z
19		cexp 12134	. . . . . . . . . . 11 class ^
20	18, 14, 19	co 6284	. . . . . . . . . 10 class ( z ^ k )
21		cmul 9497	. . . . . . . . . 10 class x.
22	17, 20, 21	co 6284	. . . . . . . . 9 class ( ( a ` k ) x. ( z ^ k ) )
23	12, 22, 13	csu 13471	. . . . . . . 8 class sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) )
24	7, 3, 23	cmpt 4505	. . . . . . 7 class ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) )
25	6, 24	wceq 1379	. . . . . 6 wff f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) )
26	2	cv 1378	. . . . . . . 8 class x
27	8	csn 4027	. . . . . . . 8 class { 0 }
28	26, 27	cun 3474	. . . . . . 7 class ( x u. { 0 } )
29		cn0 10795	. . . . . . 7 class NN0
30		cmap 7420	. . . . . . 7 class ^m
31	28, 29, 30	co 6284	. . . . . 6 class ( ( x u. { 0 } ) ^m NN0 )
32	25, 15, 31	wrex 2815	. . . . 5 wff E. a e. ( ( x u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) )
33	32, 9, 29	wrex 2815	. . . 4 wff E. n e. NN0 E. a e. ( ( x u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) )
34	33, 5	cab 2452	. . 3 class { f | E. n e. NN0 E. a e. ( ( x u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) }
35	2, 4, 34	cmpt 4505	. 2 class ( x e. ~P CC |-> { f | E. n e. NN0 E. a e. ( ( x u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) } )
36	1, 35	wceq 1379	1 wff Poly = ( x e. ~P CC |-> { f | E. n e. NN0 E. a e. ( ( x u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) } )

This definition is referenced by:  plyval  22353  plybss  22354