Definition df-ldgis 43134

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 43142. (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

Step	Hyp	Ref	Expression
1		cldgis 43133	. 2 class ldgIdlSeq
2		vr	. . 3 setvar 𝑟
3		cvv 3480	. . 3 class V
4		vi	. . . 4 setvar 𝑖
5	2	cv 1539	. . . . . 6 class 𝑟
6		cpl1 22178	. . . . . 6 class Poly1
7	5, 6	cfv 6561	. . . . 5 class (Poly1‘𝑟)
8		clidl 21216	. . . . 5 class LIdeal
9	7, 8	cfv 6561	. . . 4 class (LIdeal‘(Poly1‘𝑟))
10		vx	. . . . 5 setvar 𝑥
11		cn0 12526	. . . . 5 class ℕ0
12		vk	. . . . . . . . . . 11 setvar 𝑘
13	12	cv 1539	. . . . . . . . . 10 class 𝑘
14		cdg1 26093	. . . . . . . . . . 11 class deg1
15	5, 14	cfv 6561	. . . . . . . . . 10 class (deg1‘𝑟)
16	13, 15	cfv 6561	. . . . . . . . 9 class ((deg1‘𝑟)‘𝑘)
17	10	cv 1539	. . . . . . . . 9 class 𝑥
18		cle 11296	. . . . . . . . 9 class ≤
19	16, 17, 18	wbr 5143	. . . . . . . 8 wff ((deg1‘𝑟)‘𝑘) ≤ 𝑥
20		vj	. . . . . . . . . 10 setvar 𝑗
21	20	cv 1539	. . . . . . . . 9 class 𝑗
22		cco1 22179	. . . . . . . . . . 11 class coe1
23	13, 22	cfv 6561	. . . . . . . . . 10 class (coe1‘𝑘)
24	17, 23	cfv 6561	. . . . . . . . 9 class ((coe1‘𝑘)‘𝑥)
25	21, 24	wceq 1540	. . . . . . . 8 wff 𝑗 = ((coe1‘𝑘)‘𝑥)
26	19, 25	wa 395	. . . . . . 7 wff (((deg1‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))
27	4	cv 1539	. . . . . . 7 class 𝑖
28	26, 12, 27	wrex 3070	. . . . . 6 wff ∃𝑘 ∈ 𝑖 (((deg1‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))
29	28, 20	cab 2714	. . . . 5 class {𝑗 ∣ ∃𝑘 ∈ 𝑖 (((deg1‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))}
30	10, 11, 29	cmpt 5225	. . . 4 class (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘 ∈ 𝑖 (((deg1‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))})
31	4, 9, 30	cmpt 5225	. . 3 class (𝑖 ∈ (LIdeal‘(Poly1‘𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘 ∈ 𝑖 (((deg1‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))}))
32	2, 3, 31	cmpt 5225	. 2 class (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1‘𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘 ∈ 𝑖 (((deg1‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))})))
33	1, 32	wceq 1540	1 wff ldgIdlSeq = (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1‘𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘 ∈ 𝑖 (((deg1‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))})))

This definition is referenced by:  hbtlem1  43135  hbtlem7  43137