Definition df-mzpcl

Description: Define the polynomially closed function rings over an arbitrary index set v . The set ( mzPolyCldv ) 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 ( mzPolyv ) ; see df-mzp . (Contributed by Stefan O'Rear, 4-Oct-2014)

	Ref	Expression
Assertion	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 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmzpcl	|- mzPolyCld
1		vv	|- v
2		cvv	|- _V
3		vp	|- p
4		cz	|- ZZ
5		cmap	|- ^m
6	1	cv	|- v
7	4 6 5	co	|- ( ZZ ^m v )
8	4 7 5	co	|- ( ZZ ^m ( ZZ ^m v ) )
9	8	cpw	|- ~P ( ZZ ^m ( ZZ ^m v ) )
10		vi	|- i
11	10	cv	|- i
12	11	csn	|- { i }
13	7 12	cxp	|- ( ( ZZ ^m v ) X. { i } )
14	3	cv	|- p
15	13 14	wcel	|- ( ( ZZ ^m v ) X. { i } ) e. p
16	15 10 4	wral	|- A. i e. ZZ ( ( ZZ ^m v ) X. { i } ) e. p
17		vj	|- j
18		vx	|- x
19	18	cv	|- x
20	17	cv	|- j
21	20 19	cfv	|- ( x ` j )
22	18 7 21	cmpt	|- ( x e. ( ZZ ^m v ) |-> ( x ` j ) )
23	22 14	wcel	|- ( x e. ( ZZ ^m v ) |-> ( x ` j ) ) e. p
24	23 17 6	wral	|- A. j e. v ( x e. ( ZZ ^m v ) |-> ( x ` j ) ) e. p
25	16 24	wa	|- ( A. i e. ZZ ( ( ZZ ^m v ) X. { i } ) e. p /\ A. j e. v ( x e. ( ZZ ^m v ) |-> ( x ` j ) ) e. p )
26		vf	|- f
27		vg	|- g
28	26	cv	|- f
29		caddc	|- +
30	29	cof	|- oF +
31	27	cv	|- g
32	28 31 30	co	|- ( f oF + g )
33	32 14	wcel	|- ( f oF + g ) e. p
34		cmul	|- x.
35	34	cof	|- oF x.
36	28 31 35	co	|- ( f oF x. g )
37	36 14	wcel	|- ( f oF x. g ) e. p
38	33 37	wa	|- ( ( f oF + g ) e. p /\ ( f oF x. g ) e. p )
39	38 27 14	wral	|- A. g e. p ( ( f oF + g ) e. p /\ ( f oF x. g ) e. p )
40	39 26 14	wral	|- A. f e. p A. g e. p ( ( f oF + g ) e. p /\ ( f oF x. g ) e. p )
41	25 40	wa	|- ( ( 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 ) )
42	41 3 9	crab	|- { 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 ) ) }
43	1 2 42	cmpt	|- ( 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 ) ) } )
44	0 43	wceq	|- 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 ) ) } )