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 40059
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 40067. (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 40058 . 2 class ldgIdlSeq
2 vr . . 3 setvar 𝑟
3 cvv 3444 . . 3 class V
4 vi . . . 4 setvar 𝑖
52cv 1537 . . . . . 6 class 𝑟
6 cpl1 20810 . . . . . 6 class Poly1
75, 6cfv 6328 . . . . 5 class (Poly1𝑟)
8 clidl 19939 . . . . 5 class LIdeal
97, 8cfv 6328 . . . 4 class (LIdeal‘(Poly1𝑟))
10 vx . . . . 5 setvar 𝑥
11 cn0 11889 . . . . 5 class 0
12 vk . . . . . . . . . . 11 setvar 𝑘
1312cv 1537 . . . . . . . . . 10 class 𝑘
14 cdg1 24659 . . . . . . . . . . 11 class deg1
155, 14cfv 6328 . . . . . . . . . 10 class ( deg1𝑟)
1613, 15cfv 6328 . . . . . . . . 9 class (( deg1𝑟)‘𝑘)
1710cv 1537 . . . . . . . . 9 class 𝑥
18 cle 10669 . . . . . . . . 9 class
1916, 17, 18wbr 5033 . . . . . . . 8 wff (( deg1𝑟)‘𝑘) ≤ 𝑥
20 vj . . . . . . . . . 10 setvar 𝑗
2120cv 1537 . . . . . . . . 9 class 𝑗
22 cco1 20811 . . . . . . . . . . 11 class coe1
2313, 22cfv 6328 . . . . . . . . . 10 class (coe1𝑘)
2417, 23cfv 6328 . . . . . . . . 9 class ((coe1𝑘)‘𝑥)
2521, 24wceq 1538 . . . . . . . 8 wff 𝑗 = ((coe1𝑘)‘𝑥)
2619, 25wa 399 . . . . . . 7 wff ((( deg1𝑟)‘𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))
274cv 1537 . . . . . . 7 class 𝑖
2826, 12, 27wrex 3110 . . . . . 6 wff 𝑘𝑖 ((( deg1𝑟)‘𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))
2928, 20cab 2779 . . . . 5 class {𝑗 ∣ ∃𝑘𝑖 ((( deg1𝑟)‘𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))}
3010, 11, 29cmpt 5113 . . . 4 class (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝑖 ((( deg1𝑟)‘𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))})
314, 9, 30cmpt 5113 . . 3 class (𝑖 ∈ (LIdeal‘(Poly1𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝑖 ((( deg1𝑟)‘𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))}))
322, 3, 31cmpt 5113 . 2 class (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝑖 ((( deg1𝑟)‘𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))})))
331, 32wceq 1538 1 wff ldgIdlSeq = (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝑖 ((( deg1𝑟)‘𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))})))
Colors of variables: wff setvar class
This definition is referenced by:  hbtlem1  40060  hbtlem7  40062
  Copyright terms: Public domain W3C validator