Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ply Structured version   Unicode version

Definition df-ply 20108
 Description: Define the set of polynomials on the complexes with coefficients in the given subset. (Contributed by Mario Carneiro, 17-Jul-2014.)
Assertion
Ref Expression
df-ply Poly
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-ply
StepHypRef Expression
1 cply 20104 . 2 Poly
2 vx . . 3
3 cc 8989 . . . 4
43cpw 3800 . . 3
5 vf . . . . . . . 8
65cv 1652 . . . . . . 7
7 vz . . . . . . . 8
8 cc0 8991 . . . . . . . . . 10
9 vn . . . . . . . . . . 11
109cv 1652 . . . . . . . . . 10
11 cfz 11044 . . . . . . . . . 10
128, 10, 11co 6082 . . . . . . . . 9
13 vk . . . . . . . . . . . 12
1413cv 1652 . . . . . . . . . . 11
15 va . . . . . . . . . . . 12
1615cv 1652 . . . . . . . . . . 11
1714, 16cfv 5455 . . . . . . . . . 10
187cv 1652 . . . . . . . . . . 11
19 cexp 11383 . . . . . . . . . . 11
2018, 14, 19co 6082 . . . . . . . . . 10
21 cmul 8996 . . . . . . . . . 10
2217, 20, 21co 6082 . . . . . . . . 9
2312, 22, 13csu 12480 . . . . . . . 8
247, 3, 23cmpt 4267 . . . . . . 7
256, 24wceq 1653 . . . . . 6
262cv 1652 . . . . . . . 8
278csn 3815 . . . . . . . 8
2826, 27cun 3319 . . . . . . 7
29 cn0 10222 . . . . . . 7
30 cmap 7019 . . . . . . 7
3128, 29, 30co 6082 . . . . . 6
3225, 15, 31wrex 2707 . . . . 5
3332, 9, 29wrex 2707 . . . 4
3433, 5cab 2423 . . 3
352, 4, 34cmpt 4267 . 2
361, 35wceq 1653 1 Poly
 Colors of variables: wff set class This definition is referenced by:  plyval  20113  plybss  20114
 Copyright terms: Public domain W3C validator