Definition df-ldgis 43113

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 43121. (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 43112	. 2 class ldgIdlSeq
2		vr	. . 3 setvar 𝑟
3		cvv 3464	. . 3 class V
4		vi	. . . 4 setvar 𝑖
5	2	cv 1539	. . . . . 6 class 𝑟
6		cpl1 22117	. . . . . 6 class Poly1
7	5, 6	cfv 6536	. . . . 5 class (Poly1‘𝑟)
8		clidl 21172	. . . . 5 class LIdeal
9	7, 8	cfv 6536	. . . 4 class (LIdeal‘(Poly1‘𝑟))
10		vx	. . . . 5 setvar 𝑥
11		cn0 12506	. . . . 5 class ℕ0
12		vk	. . . . . . . . . . 11 setvar 𝑘
13	12	cv 1539	. . . . . . . . . 10 class 𝑘
14		cdg1 26016	. . . . . . . . . . 11 class deg1
15	5, 14	cfv 6536	. . . . . . . . . 10 class (deg1‘𝑟)
16	13, 15	cfv 6536	. . . . . . . . 9 class ((deg1‘𝑟)‘𝑘)
17	10	cv 1539	. . . . . . . . 9 class 𝑥
18		cle 11275	. . . . . . . . 9 class ≤
19	16, 17, 18	wbr 5124	. . . . . . . 8 wff ((deg1‘𝑟)‘𝑘) ≤ 𝑥
20		vj	. . . . . . . . . 10 setvar 𝑗
21	20	cv 1539	. . . . . . . . 9 class 𝑗
22		cco1 22118	. . . . . . . . . . 11 class coe1
23	13, 22	cfv 6536	. . . . . . . . . 10 class (coe1‘𝑘)
24	17, 23	cfv 6536	. . . . . . . . 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 3061	. . . . . 6 wff ∃𝑘 ∈ 𝑖 (((deg1‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))
29	28, 20	cab 2714	. . . . 5 class {𝑗 ∣ ∃𝑘 ∈ 𝑖 (((deg1‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))}
30	10, 11, 29	cmpt 5206	. . . 4 class (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘 ∈ 𝑖 (((deg1‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))})
31	4, 9, 30	cmpt 5206	. . 3 class (𝑖 ∈ (LIdeal‘(Poly1‘𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘 ∈ 𝑖 (((deg1‘𝑟)‘𝑘) ≤ 𝑥 ∧ 𝑗 = ((coe1‘𝑘)‘𝑥))}))
32	2, 3, 31	cmpt 5206	. 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  43114  hbtlem7  43116