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 \in V ⟼ \{p \in 𝒫 (ℤ^{(ℤ^{v})}) \| ((\forall i \in ℤ (ℤ^{v}) \times \{i\} \in p \land \forall j \in v (x \in (ℤ^{v}) ⟼ x (j)) \in p) \land \forall f \in p \forall g \in p (f +_{f} g \in p \land f \times_{f} g \in p))\})$

Detailed syntax breakdown

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

Metamath Proof Explorer

Definition df-mzpcl

Detailed syntax breakdown