Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mzpcl Structured version   Unicode version

Definition df-mzpcl 26780
 Description: Define the polynomially closed function rings over an arbitrary index set . The set mzPolyCld contains all sets of functions from to which include all constants and projections and are closed under addition and multiplication. This is a "temporary" set used to define the polynomial function ring itself mzPoly; see df-mzp 26781. (Contributed by Stefan O'Rear, 4-Oct-2014.)
Assertion
Ref Expression
df-mzpcl mzPolyCld
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-mzpcl
StepHypRef Expression
1 cmzpcl 26778 . 2 mzPolyCld
2 vv . . 3
3 cvv 2956 . . 3
4 cz 10282 . . . . . . . . . 10
52cv 1651 . . . . . . . . . 10
6 cmap 7018 . . . . . . . . . 10
74, 5, 6co 6081 . . . . . . . . 9
8 vi . . . . . . . . . . 11
98cv 1651 . . . . . . . . . 10
109csn 3814 . . . . . . . . 9
117, 10cxp 4876 . . . . . . . 8
12 vp . . . . . . . . 9
1312cv 1651 . . . . . . . 8
1411, 13wcel 1725 . . . . . . 7
1514, 8, 4wral 2705 . . . . . 6
16 vx . . . . . . . . 9
17 vj . . . . . . . . . . 11
1817cv 1651 . . . . . . . . . 10
1916cv 1651 . . . . . . . . . 10
2018, 19cfv 5454 . . . . . . . . 9
2116, 7, 20cmpt 4266 . . . . . . . 8
2221, 13wcel 1725 . . . . . . 7
2322, 17, 5wral 2705 . . . . . 6
2415, 23wa 359 . . . . 5
25 vf . . . . . . . . . . 11
2625cv 1651 . . . . . . . . . 10
27 vg . . . . . . . . . . 11
2827cv 1651 . . . . . . . . . 10
29 caddc 8993 . . . . . . . . . . 11
3029cof 6303 . . . . . . . . . 10
3126, 28, 30co 6081 . . . . . . . . 9
3231, 13wcel 1725 . . . . . . . 8
33 cmul 8995 . . . . . . . . . . 11
3433cof 6303 . . . . . . . . . 10
3526, 28, 34co 6081 . . . . . . . . 9
3635, 13wcel 1725 . . . . . . . 8
3732, 36wa 359 . . . . . . 7
3837, 27, 13wral 2705 . . . . . 6
3938, 25, 13wral 2705 . . . . 5
4024, 39wa 359 . . . 4
414, 7, 6co 6081 . . . . 5
4241cpw 3799 . . . 4
4340, 12, 42crab 2709 . . 3
442, 3, 43cmpt 4266 . 2
451, 44wceq 1652 1 mzPolyCld
 Colors of variables: wff set class This definition is referenced by:  mzpclval  26782
 Copyright terms: Public domain W3C validator