Definition df-mzpcl 37286

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

Assertion

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

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

Detailed syntax breakdown of Definition df-mzpcl

Step	Hyp	Ref	Expression
1		cmzpcl 37284	. 2 class mzPolyCld
2		vv	. . 3 setvar 𝑣
3		cvv 3200	. . 3 class V
4		cz 11377	. . . . . . . . . 10 class ℤ
5	2	cv 1482	. . . . . . . . . 10 class 𝑣
6		cmap 7857	. . . . . . . . . 10 class ↑𝑚
7	4, 5, 6	co 6650	. . . . . . . . 9 class (ℤ ↑𝑚 𝑣)
8		vi	. . . . . . . . . . 11 setvar 𝑖
9	8	cv 1482	. . . . . . . . . 10 class 𝑖
10	9	csn 4177	. . . . . . . . 9 class {𝑖}
11	7, 10	cxp 5112	. . . . . . . 8 class ((ℤ ↑𝑚 𝑣) × {𝑖})
12		vp	. . . . . . . . 9 setvar 𝑝
13	12	cv 1482	. . . . . . . 8 class 𝑝
14	11, 13	wcel 1990	. . . . . . 7 wff ((ℤ ↑𝑚 𝑣) × {𝑖}) ∈ 𝑝
15	14, 8, 4	wral 2912	. . . . . 6 wff ∀𝑖 ∈ ℤ ((ℤ ↑𝑚 𝑣) × {𝑖}) ∈ 𝑝
16		vx	. . . . . . . . 9 setvar 𝑥
17		vj	. . . . . . . . . . 11 setvar 𝑗
18	17	cv 1482	. . . . . . . . . 10 class 𝑗
19	16	cv 1482	. . . . . . . . . 10 class 𝑥
20	18, 19	cfv 5888	. . . . . . . . 9 class (𝑥‘𝑗)
21	16, 7, 20	cmpt 4729	. . . . . . . 8 class (𝑥 ∈ (ℤ ↑𝑚 𝑣) ↦ (𝑥‘𝑗))
22	21, 13	wcel 1990	. . . . . . 7 wff (𝑥 ∈ (ℤ ↑𝑚 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝
23	22, 17, 5	wral 2912	. . . . . 6 wff ∀𝑗 ∈ 𝑣 (𝑥 ∈ (ℤ ↑𝑚 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝
24	15, 23	wa 384	. . . . 5 wff (∀𝑖 ∈ ℤ ((ℤ ↑𝑚 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑣 (𝑥 ∈ (ℤ ↑𝑚 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝)
25		vf	. . . . . . . . . . 11 setvar 𝑓
26	25	cv 1482	. . . . . . . . . 10 class 𝑓
27		vg	. . . . . . . . . . 11 setvar 𝑔
28	27	cv 1482	. . . . . . . . . 10 class 𝑔
29		caddc 9939	. . . . . . . . . . 11 class +
30	29	cof 6895	. . . . . . . . . 10 class ∘𝑓 +
31	26, 28, 30	co 6650	. . . . . . . . 9 class (𝑓 ∘𝑓 + 𝑔)
32	31, 13	wcel 1990	. . . . . . . 8 wff (𝑓 ∘𝑓 + 𝑔) ∈ 𝑝
33		cmul 9941	. . . . . . . . . . 11 class ·
34	33	cof 6895	. . . . . . . . . 10 class ∘𝑓 ·
35	26, 28, 34	co 6650	. . . . . . . . 9 class (𝑓 ∘𝑓 · 𝑔)
36	35, 13	wcel 1990	. . . . . . . 8 wff (𝑓 ∘𝑓 · 𝑔) ∈ 𝑝
37	32, 36	wa 384	. . . . . . 7 wff ((𝑓 ∘𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑝)
38	37, 27, 13	wral 2912	. . . . . 6 wff ∀𝑔 ∈ 𝑝 ((𝑓 ∘𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑝)
39	38, 25, 13	wral 2912	. . . . 5 wff ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑝)
40	24, 39	wa 384	. . . 4 wff ((∀𝑖 ∈ ℤ ((ℤ ↑𝑚 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑣 (𝑥 ∈ (ℤ ↑𝑚 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑝))
41	4, 7, 6	co 6650	. . . . 5 class (ℤ ↑𝑚 (ℤ ↑𝑚 𝑣))
42	41	cpw 4158	. . . 4 class 𝒫 (ℤ ↑𝑚 (ℤ ↑𝑚 𝑣))
43	40, 12, 42	crab 2916	. . 3 class {𝑝 ∈ 𝒫 (ℤ ↑𝑚 (ℤ ↑𝑚 𝑣)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑𝑚 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑣 (𝑥 ∈ (ℤ ↑𝑚 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑝))}
44	2, 3, 43	cmpt 4729	. 2 class (𝑣 ∈ V ↦ {𝑝 ∈ 𝒫 (ℤ ↑𝑚 (ℤ ↑𝑚 𝑣)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑𝑚 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑣 (𝑥 ∈ (ℤ ↑𝑚 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑝))})
45	1, 44	wceq 1483	1 wff mzPolyCld = (𝑣 ∈ V ↦ {𝑝 ∈ 𝒫 (ℤ ↑𝑚 (ℤ ↑𝑚 𝑣)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑𝑚 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑣 (𝑥 ∈ (ℤ ↑𝑚 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘𝑓 · 𝑔) ∈ 𝑝))})

This definition is referenced by:  mzpclval  37288