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

Definition df-ldgis 41478
Description: Define a function which carries polynomial ideals to the sequence of coefficient ideals of leading coefficients of degree- π‘₯ elements in the polynomial ideal. The proof that this map is strictly monotone is the core of the Hilbert Basis Theorem hbt 41486. (Contributed by Stefan O'Rear, 31-Mar-2015.)
Assertion
Ref Expression
df-ldgis ldgIdlSeq = (π‘Ÿ ∈ V ↦ (𝑖 ∈ (LIdealβ€˜(Poly1β€˜π‘Ÿ)) ↦ (π‘₯ ∈ β„•0 ↦ {𝑗 ∣ βˆƒπ‘˜ ∈ 𝑖 ((( deg1 β€˜π‘Ÿ)β€˜π‘˜) ≀ π‘₯ ∧ 𝑗 = ((coe1β€˜π‘˜)β€˜π‘₯))})))
Distinct variable group:   𝑖,π‘Ÿ,π‘₯,𝑗,π‘˜

Detailed syntax breakdown of Definition df-ldgis
StepHypRef Expression
1 cldgis 41477 . 2 class ldgIdlSeq
2 vr . . 3 setvar π‘Ÿ
3 cvv 3448 . . 3 class V
4 vi . . . 4 setvar 𝑖
52cv 1541 . . . . . 6 class π‘Ÿ
6 cpl1 21564 . . . . . 6 class Poly1
75, 6cfv 6501 . . . . 5 class (Poly1β€˜π‘Ÿ)
8 clidl 20647 . . . . 5 class LIdeal
97, 8cfv 6501 . . . 4 class (LIdealβ€˜(Poly1β€˜π‘Ÿ))
10 vx . . . . 5 setvar π‘₯
11 cn0 12420 . . . . 5 class β„•0
12 vk . . . . . . . . . . 11 setvar π‘˜
1312cv 1541 . . . . . . . . . 10 class π‘˜
14 cdg1 25432 . . . . . . . . . . 11 class deg1
155, 14cfv 6501 . . . . . . . . . 10 class ( deg1 β€˜π‘Ÿ)
1613, 15cfv 6501 . . . . . . . . 9 class (( deg1 β€˜π‘Ÿ)β€˜π‘˜)
1710cv 1541 . . . . . . . . 9 class π‘₯
18 cle 11197 . . . . . . . . 9 class ≀
1916, 17, 18wbr 5110 . . . . . . . 8 wff (( deg1 β€˜π‘Ÿ)β€˜π‘˜) ≀ π‘₯
20 vj . . . . . . . . . 10 setvar 𝑗
2120cv 1541 . . . . . . . . 9 class 𝑗
22 cco1 21565 . . . . . . . . . . 11 class coe1
2313, 22cfv 6501 . . . . . . . . . 10 class (coe1β€˜π‘˜)
2417, 23cfv 6501 . . . . . . . . 9 class ((coe1β€˜π‘˜)β€˜π‘₯)
2521, 24wceq 1542 . . . . . . . 8 wff 𝑗 = ((coe1β€˜π‘˜)β€˜π‘₯)
2619, 25wa 397 . . . . . . 7 wff ((( deg1 β€˜π‘Ÿ)β€˜π‘˜) ≀ π‘₯ ∧ 𝑗 = ((coe1β€˜π‘˜)β€˜π‘₯))
274cv 1541 . . . . . . 7 class 𝑖
2826, 12, 27wrex 3074 . . . . . 6 wff βˆƒπ‘˜ ∈ 𝑖 ((( deg1 β€˜π‘Ÿ)β€˜π‘˜) ≀ π‘₯ ∧ 𝑗 = ((coe1β€˜π‘˜)β€˜π‘₯))
2928, 20cab 2714 . . . . 5 class {𝑗 ∣ βˆƒπ‘˜ ∈ 𝑖 ((( deg1 β€˜π‘Ÿ)β€˜π‘˜) ≀ π‘₯ ∧ 𝑗 = ((coe1β€˜π‘˜)β€˜π‘₯))}
3010, 11, 29cmpt 5193 . . . 4 class (π‘₯ ∈ β„•0 ↦ {𝑗 ∣ βˆƒπ‘˜ ∈ 𝑖 ((( deg1 β€˜π‘Ÿ)β€˜π‘˜) ≀ π‘₯ ∧ 𝑗 = ((coe1β€˜π‘˜)β€˜π‘₯))})
314, 9, 30cmpt 5193 . . 3 class (𝑖 ∈ (LIdealβ€˜(Poly1β€˜π‘Ÿ)) ↦ (π‘₯ ∈ β„•0 ↦ {𝑗 ∣ βˆƒπ‘˜ ∈ 𝑖 ((( deg1 β€˜π‘Ÿ)β€˜π‘˜) ≀ π‘₯ ∧ 𝑗 = ((coe1β€˜π‘˜)β€˜π‘₯))}))
322, 3, 31cmpt 5193 . 2 class (π‘Ÿ ∈ V ↦ (𝑖 ∈ (LIdealβ€˜(Poly1β€˜π‘Ÿ)) ↦ (π‘₯ ∈ β„•0 ↦ {𝑗 ∣ βˆƒπ‘˜ ∈ 𝑖 ((( deg1 β€˜π‘Ÿ)β€˜π‘˜) ≀ π‘₯ ∧ 𝑗 = ((coe1β€˜π‘˜)β€˜π‘₯))})))
331, 32wceq 1542 1 wff ldgIdlSeq = (π‘Ÿ ∈ V ↦ (𝑖 ∈ (LIdealβ€˜(Poly1β€˜π‘Ÿ)) ↦ (π‘₯ ∈ β„•0 ↦ {𝑗 ∣ βˆƒπ‘˜ ∈ 𝑖 ((( deg1 β€˜π‘Ÿ)β€˜π‘˜) ≀ π‘₯ ∧ 𝑗 = ((coe1β€˜π‘˜)β€˜π‘₯))})))
Colors of variables: wff setvar class
This definition is referenced by:  hbtlem1  41479  hbtlem7  41481
  Copyright terms: Public domain W3C validator