Users' Mathboxes 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 36805
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 36806. (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
StepHypRef Expression
1 cmzpcl 36803 . 2 class mzPolyCld
2 vv . . 3 setvar 𝑣
3 cvv 3190 . . 3 class V
4 cz 11337 . . . . . . . . . 10 class
52cv 1479 . . . . . . . . . 10 class 𝑣
6 cmap 7817 . . . . . . . . . 10 class 𝑚
74, 5, 6co 6615 . . . . . . . . 9 class (ℤ ↑𝑚 𝑣)
8 vi . . . . . . . . . . 11 setvar 𝑖
98cv 1479 . . . . . . . . . 10 class 𝑖
109csn 4155 . . . . . . . . 9 class {𝑖}
117, 10cxp 5082 . . . . . . . 8 class ((ℤ ↑𝑚 𝑣) × {𝑖})
12 vp . . . . . . . . 9 setvar 𝑝
1312cv 1479 . . . . . . . 8 class 𝑝
1411, 13wcel 1987 . . . . . . 7 wff ((ℤ ↑𝑚 𝑣) × {𝑖}) ∈ 𝑝
1514, 8, 4wral 2908 . . . . . 6 wff 𝑖 ∈ ℤ ((ℤ ↑𝑚 𝑣) × {𝑖}) ∈ 𝑝
16 vx . . . . . . . . 9 setvar 𝑥
17 vj . . . . . . . . . . 11 setvar 𝑗
1817cv 1479 . . . . . . . . . 10 class 𝑗
1916cv 1479 . . . . . . . . . 10 class 𝑥
2018, 19cfv 5857 . . . . . . . . 9 class (𝑥𝑗)
2116, 7, 20cmpt 4683 . . . . . . . 8 class (𝑥 ∈ (ℤ ↑𝑚 𝑣) ↦ (𝑥𝑗))
2221, 13wcel 1987 . . . . . . 7 wff (𝑥 ∈ (ℤ ↑𝑚 𝑣) ↦ (𝑥𝑗)) ∈ 𝑝
2322, 17, 5wral 2908 . . . . . 6 wff 𝑗𝑣 (𝑥 ∈ (ℤ ↑𝑚 𝑣) ↦ (𝑥𝑗)) ∈ 𝑝
2415, 23wa 384 . . . . 5 wff (∀𝑖 ∈ ℤ ((ℤ ↑𝑚 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗𝑣 (𝑥 ∈ (ℤ ↑𝑚 𝑣) ↦ (𝑥𝑗)) ∈ 𝑝)
25 vf . . . . . . . . . . 11 setvar 𝑓
2625cv 1479 . . . . . . . . . 10 class 𝑓
27 vg . . . . . . . . . . 11 setvar 𝑔
2827cv 1479 . . . . . . . . . 10 class 𝑔
29 caddc 9899 . . . . . . . . . . 11 class +
3029cof 6860 . . . . . . . . . 10 class 𝑓 +
3126, 28, 30co 6615 . . . . . . . . 9 class (𝑓𝑓 + 𝑔)
3231, 13wcel 1987 . . . . . . . 8 wff (𝑓𝑓 + 𝑔) ∈ 𝑝
33 cmul 9901 . . . . . . . . . . 11 class ·
3433cof 6860 . . . . . . . . . 10 class 𝑓 ·
3526, 28, 34co 6615 . . . . . . . . 9 class (𝑓𝑓 · 𝑔)
3635, 13wcel 1987 . . . . . . . 8 wff (𝑓𝑓 · 𝑔) ∈ 𝑝
3732, 36wa 384 . . . . . . 7 wff ((𝑓𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓𝑓 · 𝑔) ∈ 𝑝)
3837, 27, 13wral 2908 . . . . . 6 wff 𝑔𝑝 ((𝑓𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓𝑓 · 𝑔) ∈ 𝑝)
3938, 25, 13wral 2908 . . . . 5 wff 𝑓𝑝𝑔𝑝 ((𝑓𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓𝑓 · 𝑔) ∈ 𝑝)
4024, 39wa 384 . . . 4 wff ((∀𝑖 ∈ ℤ ((ℤ ↑𝑚 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗𝑣 (𝑥 ∈ (ℤ ↑𝑚 𝑣) ↦ (𝑥𝑗)) ∈ 𝑝) ∧ ∀𝑓𝑝𝑔𝑝 ((𝑓𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓𝑓 · 𝑔) ∈ 𝑝))
414, 7, 6co 6615 . . . . 5 class (ℤ ↑𝑚 (ℤ ↑𝑚 𝑣))
4241cpw 4136 . . . 4 class 𝒫 (ℤ ↑𝑚 (ℤ ↑𝑚 𝑣))
4340, 12, 42crab 2912 . . 3 class {𝑝 ∈ 𝒫 (ℤ ↑𝑚 (ℤ ↑𝑚 𝑣)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑𝑚 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗𝑣 (𝑥 ∈ (ℤ ↑𝑚 𝑣) ↦ (𝑥𝑗)) ∈ 𝑝) ∧ ∀𝑓𝑝𝑔𝑝 ((𝑓𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓𝑓 · 𝑔) ∈ 𝑝))}
442, 3, 43cmpt 4683 . 2 class (𝑣 ∈ V ↦ {𝑝 ∈ 𝒫 (ℤ ↑𝑚 (ℤ ↑𝑚 𝑣)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑𝑚 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗𝑣 (𝑥 ∈ (ℤ ↑𝑚 𝑣) ↦ (𝑥𝑗)) ∈ 𝑝) ∧ ∀𝑓𝑝𝑔𝑝 ((𝑓𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓𝑓 · 𝑔) ∈ 𝑝))})
451, 44wceq 1480 1 wff mzPolyCld = (𝑣 ∈ V ↦ {𝑝 ∈ 𝒫 (ℤ ↑𝑚 (ℤ ↑𝑚 𝑣)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑𝑚 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗𝑣 (𝑥 ∈ (ℤ ↑𝑚 𝑣) ↦ (𝑥𝑗)) ∈ 𝑝) ∧ ∀𝑓𝑝𝑔𝑝 ((𝑓𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓𝑓 · 𝑔) ∈ 𝑝))})
Colors of variables: wff setvar class
This definition is referenced by:  mzpclval  36807
  Copyright terms: Public domain W3C validator