Definition df-mzpcl 37286

Description: Define the polynomially closed function rings over an arbitrary index set v. The set (mzPolyCld ` v ) contains all sets of functions from ( ZZ ^m v ) to ZZ 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 ` v ); see df-mzp 37287. (Contributed by Stefan O'Rear, 4-Oct-2014.)

Assertion

Ref	Expression
df-mzpcl	|- mzPolyCld = ( v e. _V |-> { p e. ~P ( ZZ ^m ( ZZ ^m v ) ) | ( ( A. i e. ZZ ( ( ZZ ^m v ) X. { i } ) e. p /\ A. j e. v ( x e. ( ZZ ^m v ) |-> ( x ` j ) ) e. p ) /\ A. f e. p A. g e. p ( ( f oF + g ) e. p /\ ( f oF x. g ) e. p ) ) } )

Distinct variable group:   f, g, i, j, p, v, x

Detailed syntax breakdown of Definition df-mzpcl

Step	Hyp	Ref	Expression
1		cmzpcl 37284	. 2 class mzPolyCld
2		vv	. . 3 setvar v
3		cvv 3200	. . 3 class _V
4		cz 11377	. . . . . . . . . 10 class ZZ
5	2	cv 1482	. . . . . . . . . 10 class v
6		cmap 7857	. . . . . . . . . 10 class ^m
7	4, 5, 6	co 6650	. . . . . . . . 9 class ( ZZ ^m v )
8		vi	. . . . . . . . . . 11 setvar i
9	8	cv 1482	. . . . . . . . . 10 class i
10	9	csn 4177	. . . . . . . . 9 class { i }
11	7, 10	cxp 5112	. . . . . . . 8 class ( ( ZZ ^m v ) X. { i } )
12		vp	. . . . . . . . 9 setvar p
13	12	cv 1482	. . . . . . . 8 class p
14	11, 13	wcel 1990	. . . . . . 7 wff ( ( ZZ ^m v ) X. { i } ) e. p
15	14, 8, 4	wral 2912	. . . . . 6 wff A. i e. ZZ ( ( ZZ ^m v ) X. { i } ) e. p
16		vx	. . . . . . . . 9 setvar x
17		vj	. . . . . . . . . . 11 setvar j
18	17	cv 1482	. . . . . . . . . 10 class j
19	16	cv 1482	. . . . . . . . . 10 class x
20	18, 19	cfv 5888	. . . . . . . . 9 class ( x ` j )
21	16, 7, 20	cmpt 4729	. . . . . . . 8 class ( x e. ( ZZ ^m v ) |-> ( x ` j ) )
22	21, 13	wcel 1990	. . . . . . 7 wff ( x e. ( ZZ ^m v ) |-> ( x ` j ) ) e. p
23	22, 17, 5	wral 2912	. . . . . 6 wff A. j e. v ( x e. ( ZZ ^m v ) |-> ( x ` j ) ) e. p
24	15, 23	wa 384	. . . . 5 wff ( A. i e. ZZ ( ( ZZ ^m v ) X. { i } ) e. p /\ A. j e. v ( x e. ( ZZ ^m v ) |-> ( x ` j ) ) e. p )
25		vf	. . . . . . . . . . 11 setvar f
26	25	cv 1482	. . . . . . . . . 10 class f
27		vg	. . . . . . . . . . 11 setvar g
28	27	cv 1482	. . . . . . . . . 10 class g
29		caddc 9939	. . . . . . . . . . 11 class +
30	29	cof 6895	. . . . . . . . . 10 class oF +
31	26, 28, 30	co 6650	. . . . . . . . 9 class ( f oF + g )
32	31, 13	wcel 1990	. . . . . . . 8 wff ( f oF + g ) e. p
33		cmul 9941	. . . . . . . . . . 11 class x.
34	33	cof 6895	. . . . . . . . . 10 class oF x.
35	26, 28, 34	co 6650	. . . . . . . . 9 class ( f oF x. g )
36	35, 13	wcel 1990	. . . . . . . 8 wff ( f oF x. g ) e. p
37	32, 36	wa 384	. . . . . . 7 wff ( ( f oF + g ) e. p /\ ( f oF x. g ) e. p )
38	37, 27, 13	wral 2912	. . . . . 6 wff A. g e. p ( ( f oF + g ) e. p /\ ( f oF x. g ) e. p )
39	38, 25, 13	wral 2912	. . . . 5 wff A. f e. p A. g e. p ( ( f oF + g ) e. p /\ ( f oF x. g ) e. p )
40	24, 39	wa 384	. . . 4 wff ( ( A. i e. ZZ ( ( ZZ ^m v ) X. { i } ) e. p /\ A. j e. v ( x e. ( ZZ ^m v ) |-> ( x ` j ) ) e. p ) /\ A. f e. p A. g e. p ( ( f oF + g ) e. p /\ ( f oF x. g ) e. p ) )
41	4, 7, 6	co 6650	. . . . 5 class ( ZZ ^m ( ZZ ^m v ) )
42	41	cpw 4158	. . . 4 class ~P ( ZZ ^m ( ZZ ^m v ) )
43	40, 12, 42	crab 2916	. . 3 class { p e. ~P ( ZZ ^m ( ZZ ^m v ) ) | ( ( A. i e. ZZ ( ( ZZ ^m v ) X. { i } ) e. p /\ A. j e. v ( x e. ( ZZ ^m v ) |-> ( x ` j ) ) e. p ) /\ A. f e. p A. g e. p ( ( f oF + g ) e. p /\ ( f oF x. g ) e. p ) ) }
44	2, 3, 43	cmpt 4729	. 2 class ( v e. _V |-> { p e. ~P ( ZZ ^m ( ZZ ^m v ) ) | ( ( A. i e. ZZ ( ( ZZ ^m v ) X. { i } ) e. p /\ A. j e. v ( x e. ( ZZ ^m v ) |-> ( x ` j ) ) e. p ) /\ A. f e. p A. g e. p ( ( f oF + g ) e. p /\ ( f oF x. g ) e. p ) ) } )
45	1, 44	wceq 1483	1 wff mzPolyCld = ( v e. _V |-> { p e. ~P ( ZZ ^m ( ZZ ^m v ) ) | ( ( A. i e. ZZ ( ( ZZ ^m v ) X. { i } ) e. p /\ A. j e. v ( x e. ( ZZ ^m v ) |-> ( x ` j ) ) e. p ) /\ A. f e. p A. g e. p ( ( f oF + g ) e. p /\ ( f oF x. g ) e. p ) ) } )

This definition is referenced by:  mzpclval  37288