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 36507
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 36515. (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 36506 . 2 class ldgIdlSeq
2 vr . . 3 setvar 𝑟
3 cvv 3172 . . 3 class V
4 vi . . . 4 setvar 𝑖
52cv 1473 . . . . . 6 class 𝑟
6 cpl1 19314 . . . . . 6 class Poly1
75, 6cfv 5790 . . . . 5 class (Poly1𝑟)
8 clidl 18937 . . . . 5 class LIdeal
97, 8cfv 5790 . . . 4 class (LIdeal‘(Poly1𝑟))
10 vx . . . . 5 setvar 𝑥
11 cn0 11139 . . . . 5 class 0
12 vk . . . . . . . . . . 11 setvar 𝑘
1312cv 1473 . . . . . . . . . 10 class 𝑘
14 cdg1 23535 . . . . . . . . . . 11 class deg1
155, 14cfv 5790 . . . . . . . . . 10 class ( deg1𝑟)
1613, 15cfv 5790 . . . . . . . . 9 class (( deg1𝑟)‘𝑘)
1710cv 1473 . . . . . . . . 9 class 𝑥
18 cle 9931 . . . . . . . . 9 class
1916, 17, 18wbr 4577 . . . . . . . 8 wff (( deg1𝑟)‘𝑘) ≤ 𝑥
20 vj . . . . . . . . . 10 setvar 𝑗
2120cv 1473 . . . . . . . . 9 class 𝑗
22 cco1 19315 . . . . . . . . . . 11 class coe1
2313, 22cfv 5790 . . . . . . . . . 10 class (coe1𝑘)
2417, 23cfv 5790 . . . . . . . . 9 class ((coe1𝑘)‘𝑥)
2521, 24wceq 1474 . . . . . . . 8 wff 𝑗 = ((coe1𝑘)‘𝑥)
2619, 25wa 382 . . . . . . 7 wff ((( deg1𝑟)‘𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))
274cv 1473 . . . . . . 7 class 𝑖
2826, 12, 27wrex 2896 . . . . . 6 wff 𝑘𝑖 ((( deg1𝑟)‘𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))
2928, 20cab 2595 . . . . 5 class {𝑗 ∣ ∃𝑘𝑖 ((( deg1𝑟)‘𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))}
3010, 11, 29cmpt 4637 . . . 4 class (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝑖 ((( deg1𝑟)‘𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))})
314, 9, 30cmpt 4637 . . 3 class (𝑖 ∈ (LIdeal‘(Poly1𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝑖 ((( deg1𝑟)‘𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))}))
322, 3, 31cmpt 4637 . 2 class (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝑖 ((( deg1𝑟)‘𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))})))
331, 32wceq 1474 1 wff ldgIdlSeq = (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝑖 ((( deg1𝑟)‘𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))})))
Colors of variables: wff setvar class
This definition is referenced by:  hbtlem1  36508  hbtlem7  36510
  Copyright terms: Public domain W3C validator