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 37805
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 37806. (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 37803 . 2 class mzPolyCld
2 vv . . 3 setvar 𝑣
3 cvv 3349 . . 3 class V
4 cz 11578 . . . . . . . . . 10 class
52cv 1629 . . . . . . . . . 10 class 𝑣
6 cmap 8008 . . . . . . . . . 10 class 𝑚
74, 5, 6co 6792 . . . . . . . . 9 class (ℤ ↑𝑚 𝑣)
8 vi . . . . . . . . . . 11 setvar 𝑖
98cv 1629 . . . . . . . . . 10 class 𝑖
109csn 4314 . . . . . . . . 9 class {𝑖}
117, 10cxp 5247 . . . . . . . 8 class ((ℤ ↑𝑚 𝑣) × {𝑖})
12 vp . . . . . . . . 9 setvar 𝑝
1312cv 1629 . . . . . . . 8 class 𝑝
1411, 13wcel 2144 . . . . . . 7 wff ((ℤ ↑𝑚 𝑣) × {𝑖}) ∈ 𝑝
1514, 8, 4wral 3060 . . . . . 6 wff 𝑖 ∈ ℤ ((ℤ ↑𝑚 𝑣) × {𝑖}) ∈ 𝑝
16 vx . . . . . . . . 9 setvar 𝑥
17 vj . . . . . . . . . . 11 setvar 𝑗
1817cv 1629 . . . . . . . . . 10 class 𝑗
1916cv 1629 . . . . . . . . . 10 class 𝑥
2018, 19cfv 6031 . . . . . . . . 9 class (𝑥𝑗)
2116, 7, 20cmpt 4861 . . . . . . . 8 class (𝑥 ∈ (ℤ ↑𝑚 𝑣) ↦ (𝑥𝑗))
2221, 13wcel 2144 . . . . . . 7 wff (𝑥 ∈ (ℤ ↑𝑚 𝑣) ↦ (𝑥𝑗)) ∈ 𝑝
2322, 17, 5wral 3060 . . . . . 6 wff 𝑗𝑣 (𝑥 ∈ (ℤ ↑𝑚 𝑣) ↦ (𝑥𝑗)) ∈ 𝑝
2415, 23wa 382 . . . . 5 wff (∀𝑖 ∈ ℤ ((ℤ ↑𝑚 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗𝑣 (𝑥 ∈ (ℤ ↑𝑚 𝑣) ↦ (𝑥𝑗)) ∈ 𝑝)
25 vf . . . . . . . . . . 11 setvar 𝑓
2625cv 1629 . . . . . . . . . 10 class 𝑓
27 vg . . . . . . . . . . 11 setvar 𝑔
2827cv 1629 . . . . . . . . . 10 class 𝑔
29 caddc 10140 . . . . . . . . . . 11 class +
3029cof 7041 . . . . . . . . . 10 class 𝑓 +
3126, 28, 30co 6792 . . . . . . . . 9 class (𝑓𝑓 + 𝑔)
3231, 13wcel 2144 . . . . . . . 8 wff (𝑓𝑓 + 𝑔) ∈ 𝑝
33 cmul 10142 . . . . . . . . . . 11 class ·
3433cof 7041 . . . . . . . . . 10 class 𝑓 ·
3526, 28, 34co 6792 . . . . . . . . 9 class (𝑓𝑓 · 𝑔)
3635, 13wcel 2144 . . . . . . . 8 wff (𝑓𝑓 · 𝑔) ∈ 𝑝
3732, 36wa 382 . . . . . . 7 wff ((𝑓𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓𝑓 · 𝑔) ∈ 𝑝)
3837, 27, 13wral 3060 . . . . . 6 wff 𝑔𝑝 ((𝑓𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓𝑓 · 𝑔) ∈ 𝑝)
3938, 25, 13wral 3060 . . . . 5 wff 𝑓𝑝𝑔𝑝 ((𝑓𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓𝑓 · 𝑔) ∈ 𝑝)
4024, 39wa 382 . . . 4 wff ((∀𝑖 ∈ ℤ ((ℤ ↑𝑚 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗𝑣 (𝑥 ∈ (ℤ ↑𝑚 𝑣) ↦ (𝑥𝑗)) ∈ 𝑝) ∧ ∀𝑓𝑝𝑔𝑝 ((𝑓𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓𝑓 · 𝑔) ∈ 𝑝))
414, 7, 6co 6792 . . . . 5 class (ℤ ↑𝑚 (ℤ ↑𝑚 𝑣))
4241cpw 4295 . . . 4 class 𝒫 (ℤ ↑𝑚 (ℤ ↑𝑚 𝑣))
4340, 12, 42crab 3064 . . 3 class {𝑝 ∈ 𝒫 (ℤ ↑𝑚 (ℤ ↑𝑚 𝑣)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑𝑚 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗𝑣 (𝑥 ∈ (ℤ ↑𝑚 𝑣) ↦ (𝑥𝑗)) ∈ 𝑝) ∧ ∀𝑓𝑝𝑔𝑝 ((𝑓𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓𝑓 · 𝑔) ∈ 𝑝))}
442, 3, 43cmpt 4861 . 2 class (𝑣 ∈ V ↦ {𝑝 ∈ 𝒫 (ℤ ↑𝑚 (ℤ ↑𝑚 𝑣)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑𝑚 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗𝑣 (𝑥 ∈ (ℤ ↑𝑚 𝑣) ↦ (𝑥𝑗)) ∈ 𝑝) ∧ ∀𝑓𝑝𝑔𝑝 ((𝑓𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓𝑓 · 𝑔) ∈ 𝑝))})
451, 44wceq 1630 1 wff mzPolyCld = (𝑣 ∈ V ↦ {𝑝 ∈ 𝒫 (ℤ ↑𝑚 (ℤ ↑𝑚 𝑣)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑𝑚 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗𝑣 (𝑥 ∈ (ℤ ↑𝑚 𝑣) ↦ (𝑥𝑗)) ∈ 𝑝) ∧ ∀𝑓𝑝𝑔𝑝 ((𝑓𝑓 + 𝑔) ∈ 𝑝 ∧ (𝑓𝑓 · 𝑔) ∈ 𝑝))})
Colors of variables: wff setvar class
This definition is referenced by:  mzpclval  37807
  Copyright terms: Public domain W3C validator