Definition df-mzpcl 42734

Description: Define the polynomially closed function rings over an arbitrary index set 𝑣. The set (mzPolyCld‘𝑣) contains all sets of functions from (ℤ ↑_m 𝑣) 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 42735. (Contributed by Stefan O'Rear, 4-Oct-2014.)

Assertion

Ref	Expression
df-mzpcl	⊢ mzPolyCld = (𝑣 ∈ V ↦ {𝑝 ∈ 𝒫 (ℤ ↑m (ℤ ↑m 𝑣)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑m 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑣 (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝))})

Distinct variable group:   𝑓,𝑔,𝑖,𝑗,𝑝,𝑣,𝑥

Detailed syntax breakdown of Definition df-mzpcl

Step	Hyp	Ref	Expression
1		cmzpcl 42732	. 2 class mzPolyCld
2		vv	. . 3 setvar 𝑣
3		cvv 3480	. . 3 class V
4		cz 12613	. . . . . . . . . 10 class ℤ
5	2	cv 1539	. . . . . . . . . 10 class 𝑣
6		cmap 8866	. . . . . . . . . 10 class ↑m
7	4, 5, 6	co 7431	. . . . . . . . 9 class (ℤ ↑m 𝑣)
8		vi	. . . . . . . . . . 11 setvar 𝑖
9	8	cv 1539	. . . . . . . . . 10 class 𝑖
10	9	csn 4626	. . . . . . . . 9 class {𝑖}
11	7, 10	cxp 5683	. . . . . . . 8 class ((ℤ ↑m 𝑣) × {𝑖})
12		vp	. . . . . . . . 9 setvar 𝑝
13	12	cv 1539	. . . . . . . 8 class 𝑝
14	11, 13	wcel 2108	. . . . . . 7 wff ((ℤ ↑m 𝑣) × {𝑖}) ∈ 𝑝
15	14, 8, 4	wral 3061	. . . . . 6 wff ∀𝑖 ∈ ℤ ((ℤ ↑m 𝑣) × {𝑖}) ∈ 𝑝
16		vx	. . . . . . . . 9 setvar 𝑥
17		vj	. . . . . . . . . . 11 setvar 𝑗
18	17	cv 1539	. . . . . . . . . 10 class 𝑗
19	16	cv 1539	. . . . . . . . . 10 class 𝑥
20	18, 19	cfv 6561	. . . . . . . . 9 class (𝑥‘𝑗)
21	16, 7, 20	cmpt 5225	. . . . . . . 8 class (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥‘𝑗))
22	21, 13	wcel 2108	. . . . . . 7 wff (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝
23	22, 17, 5	wral 3061	. . . . . 6 wff ∀𝑗 ∈ 𝑣 (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝
24	15, 23	wa 395	. . . . 5 wff (∀𝑖 ∈ ℤ ((ℤ ↑m 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑣 (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝)
25		vf	. . . . . . . . . . 11 setvar 𝑓
26	25	cv 1539	. . . . . . . . . 10 class 𝑓
27		vg	. . . . . . . . . . 11 setvar 𝑔
28	27	cv 1539	. . . . . . . . . 10 class 𝑔
29		caddc 11158	. . . . . . . . . . 11 class +
30	29	cof 7695	. . . . . . . . . 10 class ∘f +
31	26, 28, 30	co 7431	. . . . . . . . 9 class (𝑓 ∘f + 𝑔)
32	31, 13	wcel 2108	. . . . . . . 8 wff (𝑓 ∘f + 𝑔) ∈ 𝑝
33		cmul 11160	. . . . . . . . . . 11 class ·
34	33	cof 7695	. . . . . . . . . 10 class ∘f ·
35	26, 28, 34	co 7431	. . . . . . . . 9 class (𝑓 ∘f · 𝑔)
36	35, 13	wcel 2108	. . . . . . . 8 wff (𝑓 ∘f · 𝑔) ∈ 𝑝
37	32, 36	wa 395	. . . . . . 7 wff ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝)
38	37, 27, 13	wral 3061	. . . . . 6 wff ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝)
39	38, 25, 13	wral 3061	. . . . 5 wff ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝)
40	24, 39	wa 395	. . . 4 wff ((∀𝑖 ∈ ℤ ((ℤ ↑m 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑣 (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝))
41	4, 7, 6	co 7431	. . . . 5 class (ℤ ↑m (ℤ ↑m 𝑣))
42	41	cpw 4600	. . . 4 class 𝒫 (ℤ ↑m (ℤ ↑m 𝑣))
43	40, 12, 42	crab 3436	. . 3 class {𝑝 ∈ 𝒫 (ℤ ↑m (ℤ ↑m 𝑣)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑m 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑣 (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝))}
44	2, 3, 43	cmpt 5225	. 2 class (𝑣 ∈ V ↦ {𝑝 ∈ 𝒫 (ℤ ↑m (ℤ ↑m 𝑣)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑m 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑣 (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝))})
45	1, 44	wceq 1540	1 wff mzPolyCld = (𝑣 ∈ V ↦ {𝑝 ∈ 𝒫 (ℤ ↑m (ℤ ↑m 𝑣)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑m 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑣 (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝))})

This definition is referenced by:  mzpclval  42736