Metamath Proof Explorer

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 
|- 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 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cply 
 |-  Poly
1 vx 
 |-  x
2 cc 
 |-  CC
3 2 cpw 
 |-  ~P CC
4 vf 
 |-  f
5 vn 
 |-  n
6 cn0 
 |-  NN0
7 va 
 |-  a
8 1 cv 
 |-  x
9 cc0 
 |-  0
10 9 csn 
 |-  { 0 }
11 8 10 cun 
 |-  ( x u. { 0 } )
12 cmap 
 |-  ^m
13 11 6 12 co 
 |-  ( ( x u. { 0 } ) ^m NN0 )
14 4 cv 
 |-  f
15 vz 
 |-  z
16 vk 
 |-  k
17 cfz 
 |-  ...
18 5 cv 
 |-  n
19 9 18 17 co 
 |-  ( 0 ... n )
20 7 cv 
 |-  a
21 16 cv 
 |-  k
22 21 20 cfv 
 |-  ( a ` k )
23 cmul 
 |-  x.
24 15 cv 
 |-  z
25 cexp 
 |-  ^
26 24 21 25 co 
 |-  ( z ^ k )
27 22 26 23 co 
 |-  ( ( a ` k ) x. ( z ^ k ) )
28 19 27 16 csu 
 |-  sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) )
29 15 2 28 cmpt 
 |-  ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) )
30 14 29 wceq 
 |-  f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) )
31 30 7 13 wrex 
 |-  E. a e. ( ( x u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) )
32 31 5 6 wrex 
 |-  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 ) ) )
33 32 4 cab 
 |-  { 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 ) ) ) }
34 1 3 33 cmpt 
 |-  ( 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 ) ) ) } )
35 0 34 wceq 
 |-  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 ) ) ) } )