Definition df-ldgis 36711

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 36719. (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 36710	. 2 class ldgIdlSeq
2		vr	. . 3 setvar 𝑟
3		cvv 3173	. . 3 class V
4		vi	. . . 4 setvar 𝑖
5	2	cv 1474	. . . . . 6 class 𝑟
6		cpl1 19368	. . . . . 6 class Poly1
7	5, 6	cfv 5804	. . . . 5 class (Poly1‘𝑟)
8		clidl 18991	. . . . 5 class LIdeal
9	7, 8	cfv 5804	. . . 4 class (LIdeal‘(Poly1‘𝑟))
10		vx	. . . . 5 setvar 𝑥
11		cn0 11169	. . . . 5 class ℕ0
12		vk	. . . . . . . . . . 11 setvar 𝑘
13	12	cv 1474	. . . . . . . . . 10 class 𝑘
14		cdg1 23618	. . . . . . . . . . 11 class deg1
15	5, 14	cfv 5804	. . . . . . . . . 10 class ( deg1 ‘𝑟)
16	13, 15	cfv 5804	. . . . . . . . 9 class (( deg1 ‘𝑟)‘𝑘)
17	10	cv 1474	. . . . . . . . 9 class 𝑥
18		cle 9954	. . . . . . . . 9 class ≤
19	16, 17, 18	wbr 4583	. . . . . . . 8 wff (( deg1 ‘𝑟)‘𝑘) ≤ 𝑥
20		vj	. . . . . . . . . 10 setvar 𝑗
21	20	cv 1474	. . . . . . . . 9 class 𝑗
22		cco1 19369	. . . . . . . . . . 11 class coe1
23	13, 22	cfv 5804	. . . . . . . . . 10 class (coe1‘𝑘)
24	17, 23	cfv 5804	. . . . . . . . 9 class ((coe1‘𝑘)‘𝑥)
25	21, 24	wceq 1475	. . . . . . . 8 wff 𝑗 = ((coe1‘𝑘)‘𝑥)
26	19, 25	wa 383	. . . . . . 7 wff ((( deg1 ‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))
27	4	cv 1474	. . . . . . 7 class 𝑖
28	26, 12, 27	wrex 2897	. . . . . 6 wff ∃𝑘 ∈ 𝑖 ((( deg1 ‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))
29	28, 20	cab 2596	. . . . 5 class {𝑗 ∣ ∃𝑘 ∈ 𝑖 ((( deg1 ‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))}
30	10, 11, 29	cmpt 4643	. . . 4 class (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘 ∈ 𝑖 ((( deg1 ‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))})
31	4, 9, 30	cmpt 4643	. . 3 class (𝑖 ∈ (LIdeal‘(Poly1‘𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘 ∈ 𝑖 ((( deg1 ‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))}))
32	2, 3, 31	cmpt 4643	. 2 class (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1‘𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘 ∈ 𝑖 ((( deg1 ‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))})))
33	1, 32	wceq 1475	1 wff ldgIdlSeq = (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1‘𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘 ∈ 𝑖 ((( deg1 ‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))})))

This definition is referenced by:  hbtlem1  36712  hbtlem7  36714