Definition df-ldgis 39728

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 39736. (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 39727	. 2 class ldgIdlSeq
2		vr	. . 3 setvar 𝑟
3		cvv 3497	. . 3 class V
4		vi	. . . 4 setvar 𝑖
5	2	cv 1535	. . . . . 6 class 𝑟
6		cpl1 20348	. . . . . 6 class Poly1
7	5, 6	cfv 6358	. . . . 5 class (Poly1‘𝑟)
8		clidl 19945	. . . . 5 class LIdeal
9	7, 8	cfv 6358	. . . 4 class (LIdeal‘(Poly1‘𝑟))
10		vx	. . . . 5 setvar 𝑥
11		cn0 11900	. . . . 5 class ℕ0
12		vk	. . . . . . . . . . 11 setvar 𝑘
13	12	cv 1535	. . . . . . . . . 10 class 𝑘
14		cdg1 24651	. . . . . . . . . . 11 class deg1
15	5, 14	cfv 6358	. . . . . . . . . 10 class ( deg1 ‘𝑟)
16	13, 15	cfv 6358	. . . . . . . . 9 class (( deg1 ‘𝑟)‘𝑘)
17	10	cv 1535	. . . . . . . . 9 class 𝑥
18		cle 10679	. . . . . . . . 9 class ≤
19	16, 17, 18	wbr 5069	. . . . . . . 8 wff (( deg1 ‘𝑟)‘𝑘) ≤ 𝑥
20		vj	. . . . . . . . . 10 setvar 𝑗
21	20	cv 1535	. . . . . . . . 9 class 𝑗
22		cco1 20349	. . . . . . . . . . 11 class coe1
23	13, 22	cfv 6358	. . . . . . . . . 10 class (coe1‘𝑘)
24	17, 23	cfv 6358	. . . . . . . . 9 class ((coe1‘𝑘)‘𝑥)
25	21, 24	wceq 1536	. . . . . . . 8 wff 𝑗 = ((coe1‘𝑘)‘𝑥)
26	19, 25	wa 398	. . . . . . 7 wff ((( deg1 ‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))
27	4	cv 1535	. . . . . . 7 class 𝑖
28	26, 12, 27	wrex 3142	. . . . . 6 wff ∃𝑘 ∈ 𝑖 ((( deg1 ‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))
29	28, 20	cab 2802	. . . . 5 class {𝑗 ∣ ∃𝑘 ∈ 𝑖 ((( deg1 ‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))}
30	10, 11, 29	cmpt 5149	. . . 4 class (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘 ∈ 𝑖 ((( deg1 ‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))})
31	4, 9, 30	cmpt 5149	. . 3 class (𝑖 ∈ (LIdeal‘(Poly1‘𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘 ∈ 𝑖 ((( deg1 ‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))}))
32	2, 3, 31	cmpt 5149	. 2 class (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1‘𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘 ∈ 𝑖 ((( deg1 ‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))})))
33	1, 32	wceq 1536	1 wff ldgIdlSeq = (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1‘𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘 ∈ 𝑖 ((( deg1 ‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))})))

This definition is referenced by:  hbtlem1  39729  hbtlem7  39731