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	$$⊢\mathrm{mzPolyCld}=\left(v\in \mathrm{V}⟼\left\{p\in 𝒫\left({\mathbb{Z}}^{\left({\mathbb{Z}}^v\right)}\right)|\left(\left(\forall i\in \mathbb{Z}\left({\mathbb{Z}}^v\right)\times \left\{i\right\}\in p\wedge \forall j\in v\left(x\in \left({\mathbb{Z}}^v\right)⟼x\left(j\right)\right)\in p\right)\wedge \forall f\in p\forall g\in p\left(f{+}_{f}g\in p\wedge f{\times }_{f}g\in p\right)\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmzpcl	$$class\mathrm{mzPolyCld}$$
1		vv	$$setvarv$$
2		cvv	$$class\mathrm{V}$$
3		vp	$$setvarp$$
4		cz	$$class\mathbb{Z}$$
5		cmap	$$class{\uparrow }_{𝑚}$$
6	1	cv	$$setvarv$$
7	4 6 5	co	$$class\left({\mathbb{Z}}^v\right)$$
8	4 7 5	co	$$class\left({\mathbb{Z}}^{\left({\mathbb{Z}}^v\right)}\right)$$
9	8	cpw	$$class𝒫\left({\mathbb{Z}}^{\left({\mathbb{Z}}^v\right)}\right)$$
10		vi	$$setvari$$
11	10	cv	$$setvari$$
12	11	csn	$$class\left\{i\right\}$$
13	7 12	cxp	$$class\left(\left({\mathbb{Z}}^v\right)\times \left\{i\right\}\right)$$
14	3	cv	$$setvarp$$
15	13 14	wcel	$$wff\left({\mathbb{Z}}^v\right)\times \left\{i\right\}\in p$$
16	15 10 4	wral	$$wff\forall i\in \mathbb{Z}\left({\mathbb{Z}}^v\right)\times \left\{i\right\}\in p$$
17		vj	$$setvarj$$
18		vx	$$setvarx$$
19	18	cv	$$setvarx$$
20	17	cv	$$setvarj$$
21	20 19	cfv	$$classx\left(j\right)$$
22	18 7 21	cmpt	$$class\left(x\in \left({\mathbb{Z}}^v\right)⟼x\left(j\right)\right)$$
23	22 14	wcel	$$wff\left(x\in \left({\mathbb{Z}}^v\right)⟼x\left(j\right)\right)\in p$$
24	23 17 6	wral	$$wff\forall j\in v\left(x\in \left({\mathbb{Z}}^v\right)⟼x\left(j\right)\right)\in p$$
25	16 24	wa	$$wff\left(\forall i\in \mathbb{Z}\left({\mathbb{Z}}^v\right)\times \left\{i\right\}\in p\wedge \forall j\in v\left(x\in \left({\mathbb{Z}}^v\right)⟼x\left(j\right)\right)\in p\right)$$
26		vf	$$setvarf$$
27		vg	$$setvarg$$
28	26	cv	$$setvarf$$
29		caddc	$$class+$$
30	29	cof	$$class{\circ }_f+$$
31	27	cv	$$setvarg$$
32	28 31 30	co	$$class\left(f{+}_{f}g\right)$$
33	32 14	wcel	$$wfff{+}_{f}g\in p$$
34		cmul	$$class\times$$
35	34	cof	$$class{\circ }_f\times$$
36	28 31 35	co	$$class\left(f{\times }_{f}g\right)$$
37	36 14	wcel	$$wfff{\times }_{f}g\in p$$
38	33 37	wa	$$wff\left(f{+}_{f}g\in p\wedge f{\times }_{f}g\in p\right)$$
39	38 27 14	wral	$$wff\forall g\in p\left(f{+}_{f}g\in p\wedge f{\times }_{f}g\in p\right)$$
40	39 26 14	wral	$$wff\forall f\in p\forall g\in p\left(f{+}_{f}g\in p\wedge f{\times }_{f}g\in p\right)$$
41	25 40	wa	$$wff\left(\left(\forall i\in \mathbb{Z}\left({\mathbb{Z}}^v\right)\times \left\{i\right\}\in p\wedge \forall j\in v\left(x\in \left({\mathbb{Z}}^v\right)⟼x\left(j\right)\right)\in p\right)\wedge \forall f\in p\forall g\in p\left(f{+}_{f}g\in p\wedge f{\times }_{f}g\in p\right)\right)$$
42	41 3 9	crab	$$class\left\{p\in 𝒫\left({\mathbb{Z}}^{\left({\mathbb{Z}}^v\right)}\right)|\left(\left(\forall i\in \mathbb{Z}\left({\mathbb{Z}}^v\right)\times \left\{i\right\}\in p\wedge \forall j\in v\left(x\in \left({\mathbb{Z}}^v\right)⟼x\left(j\right)\right)\in p\right)\wedge \forall f\in p\forall g\in p\left(f{+}_{f}g\in p\wedge f{\times }_{f}g\in p\right)\right)\right\}$$
43	1 2 42	cmpt	$$class\left(v\in \mathrm{V}⟼\left\{p\in 𝒫\left({\mathbb{Z}}^{\left({\mathbb{Z}}^v\right)}\right)|\left(\left(\forall i\in \mathbb{Z}\left({\mathbb{Z}}^v\right)\times \left\{i\right\}\in p\wedge \forall j\in v\left(x\in \left({\mathbb{Z}}^v\right)⟼x\left(j\right)\right)\in p\right)\wedge \forall f\in p\forall g\in p\left(f{+}_{f}g\in p\wedge f{\times }_{f}g\in p\right)\right)\right\}\right)$$
44	0 43	wceq	$$wff\mathrm{mzPolyCld}=\left(v\in \mathrm{V}⟼\left\{p\in 𝒫\left({\mathbb{Z}}^{\left({\mathbb{Z}}^v\right)}\right)|\left(\left(\forall i\in \mathbb{Z}\left({\mathbb{Z}}^v\right)\times \left\{i\right\}\in p\wedge \forall j\in v\left(x\in \left({\mathbb{Z}}^v\right)⟼x\left(j\right)\right)\in p\right)\wedge \forall f\in p\forall g\in p\left(f{+}_{f}g\in p\wedge f{\times }_{f}g\in p\right)\right)\right\}\right)$$