Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mzpcl Structured version   Visualization version   GIF version

Definition df-mzpcl 39707
 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 39708. (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
StepHypRef Expression
1 cmzpcl 39705 . 2 class mzPolyCld
2 vv . . 3 setvar 𝑣
3 cvv 3441 . . 3 class V
4 cz 11972 . . . . . . . . . 10 class
52cv 1537 . . . . . . . . . 10 class 𝑣
6 cmap 8392 . . . . . . . . . 10 class m
74, 5, 6co 7136 . . . . . . . . 9 class (ℤ ↑m 𝑣)
8 vi . . . . . . . . . . 11 setvar 𝑖
98cv 1537 . . . . . . . . . 10 class 𝑖
109csn 4525 . . . . . . . . 9 class {𝑖}
117, 10cxp 5518 . . . . . . . 8 class ((ℤ ↑m 𝑣) × {𝑖})
12 vp . . . . . . . . 9 setvar 𝑝
1312cv 1537 . . . . . . . 8 class 𝑝
1411, 13wcel 2111 . . . . . . 7 wff ((ℤ ↑m 𝑣) × {𝑖}) ∈ 𝑝
1514, 8, 4wral 3106 . . . . . 6 wff 𝑖 ∈ ℤ ((ℤ ↑m 𝑣) × {𝑖}) ∈ 𝑝
16 vx . . . . . . . . 9 setvar 𝑥
17 vj . . . . . . . . . . 11 setvar 𝑗
1817cv 1537 . . . . . . . . . 10 class 𝑗
1916cv 1537 . . . . . . . . . 10 class 𝑥
2018, 19cfv 6325 . . . . . . . . 9 class (𝑥𝑗)
2116, 7, 20cmpt 5111 . . . . . . . 8 class (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥𝑗))
2221, 13wcel 2111 . . . . . . 7 wff (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥𝑗)) ∈ 𝑝
2322, 17, 5wral 3106 . . . . . 6 wff 𝑗𝑣 (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥𝑗)) ∈ 𝑝
2415, 23wa 399 . . . . 5 wff (∀𝑖 ∈ ℤ ((ℤ ↑m 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗𝑣 (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥𝑗)) ∈ 𝑝)
25 vf . . . . . . . . . . 11 setvar 𝑓
2625cv 1537 . . . . . . . . . 10 class 𝑓
27 vg . . . . . . . . . . 11 setvar 𝑔
2827cv 1537 . . . . . . . . . 10 class 𝑔
29 caddc 10532 . . . . . . . . . . 11 class +
3029cof 7389 . . . . . . . . . 10 class f +
3126, 28, 30co 7136 . . . . . . . . 9 class (𝑓f + 𝑔)
3231, 13wcel 2111 . . . . . . . 8 wff (𝑓f + 𝑔) ∈ 𝑝
33 cmul 10534 . . . . . . . . . . 11 class ·
3433cof 7389 . . . . . . . . . 10 class f ·
3526, 28, 34co 7136 . . . . . . . . 9 class (𝑓f · 𝑔)
3635, 13wcel 2111 . . . . . . . 8 wff (𝑓f · 𝑔) ∈ 𝑝
3732, 36wa 399 . . . . . . 7 wff ((𝑓f + 𝑔) ∈ 𝑝 ∧ (𝑓f · 𝑔) ∈ 𝑝)
3837, 27, 13wral 3106 . . . . . 6 wff 𝑔𝑝 ((𝑓f + 𝑔) ∈ 𝑝 ∧ (𝑓f · 𝑔) ∈ 𝑝)
3938, 25, 13wral 3106 . . . . 5 wff 𝑓𝑝𝑔𝑝 ((𝑓f + 𝑔) ∈ 𝑝 ∧ (𝑓f · 𝑔) ∈ 𝑝)
4024, 39wa 399 . . . 4 wff ((∀𝑖 ∈ ℤ ((ℤ ↑m 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗𝑣 (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥𝑗)) ∈ 𝑝) ∧ ∀𝑓𝑝𝑔𝑝 ((𝑓f + 𝑔) ∈ 𝑝 ∧ (𝑓f · 𝑔) ∈ 𝑝))
414, 7, 6co 7136 . . . . 5 class (ℤ ↑m (ℤ ↑m 𝑣))
4241cpw 4497 . . . 4 class 𝒫 (ℤ ↑m (ℤ ↑m 𝑣))
4340, 12, 42crab 3110 . . 3 class {𝑝 ∈ 𝒫 (ℤ ↑m (ℤ ↑m 𝑣)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑m 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗𝑣 (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥𝑗)) ∈ 𝑝) ∧ ∀𝑓𝑝𝑔𝑝 ((𝑓f + 𝑔) ∈ 𝑝 ∧ (𝑓f · 𝑔) ∈ 𝑝))}
442, 3, 43cmpt 5111 . 2 class (𝑣 ∈ V ↦ {𝑝 ∈ 𝒫 (ℤ ↑m (ℤ ↑m 𝑣)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑m 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗𝑣 (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥𝑗)) ∈ 𝑝) ∧ ∀𝑓𝑝𝑔𝑝 ((𝑓f + 𝑔) ∈ 𝑝 ∧ (𝑓f · 𝑔) ∈ 𝑝))})
451, 44wceq 1538 1 wff mzPolyCld = (𝑣 ∈ V ↦ {𝑝 ∈ 𝒫 (ℤ ↑m (ℤ ↑m 𝑣)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑m 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗𝑣 (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥𝑗)) ∈ 𝑝) ∧ ∀𝑓𝑝𝑔𝑝 ((𝑓f + 𝑔) ∈ 𝑝 ∧ (𝑓f · 𝑔) ∈ 𝑝))})
 Colors of variables: wff setvar class This definition is referenced by:  mzpclval  39709
 Copyright terms: Public domain W3C validator