Definition df-ldgis

Description: Define a function which carries polynomial ideals to the sequence of coefficient ideals of leading coefficients of degree- x elements in the polynomial ideal. The proof that this map is strictly monotone is the core of the Hilbert Basis Theorem hbt . (Contributed by Stefan O'Rear, 31-Mar-2015)

	Ref	Expression
Assertion	df-ldgis	$$⊢\mathrm{ldgIdlSeq}=\left(r\in \mathrm{V}⟼\left(i\in \mathrm{LIdeal}\left({\mathrm{Poly}}_1\left(r\right)\right)⟼\left(x\in {\mathbb{N}}_0⟼\left\{j|\exists k\in i\left({\mathrm{deg}}_1\left(r\right)\left(k\right)\le x\wedge j={\mathrm{coe}}_1\left(k\right)\left(x\right)\right)\right\}\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cldgis	$$class\mathrm{ldgIdlSeq}$$
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		vi	$$setvari$$
4		clidl	$$class\mathrm{LIdeal}$$
5		cpl1	$$class{\mathrm{Poly}}_1$$
6	1	cv	$$setvarr$$
7	6 5	cfv	$$class{\mathrm{Poly}}_1\left(r\right)$$
8	7 4	cfv	$$class\mathrm{LIdeal}\left({\mathrm{Poly}}_1\left(r\right)\right)$$
9		vx	$$setvarx$$
10		cn0	$$class{\mathbb{N}}_0$$
11		vj	$$setvarj$$
12		vk	$$setvark$$
13	3	cv	$$setvari$$
14		cdg1	$$class{\mathrm{deg}}_1$$
15	6 14	cfv	$$class{\mathrm{deg}}_1\left(r\right)$$
16	12	cv	$$setvark$$
17	16 15	cfv	$$class{\mathrm{deg}}_1\left(r\right)\left(k\right)$$
18		cle	$$class\le$$
19	9	cv	$$setvarx$$
20	17 19 18	wbr	$$wff{\mathrm{deg}}_1\left(r\right)\left(k\right)\le x$$
21	11	cv	$$setvarj$$
22		cco1	$$class{\mathrm{coe}}_1$$
23	16 22	cfv	$$class{\mathrm{coe}}_1\left(k\right)$$
24	19 23	cfv	$$class{\mathrm{coe}}_1\left(k\right)\left(x\right)$$
25	21 24	wceq	$$wffj={\mathrm{coe}}_1\left(k\right)\left(x\right)$$
26	20 25	wa	$$wff\left({\mathrm{deg}}_1\left(r\right)\left(k\right)\le x\wedge j={\mathrm{coe}}_1\left(k\right)\left(x\right)\right)$$
27	26 12 13	wrex	$$wff\exists k\in i\left({\mathrm{deg}}_1\left(r\right)\left(k\right)\le x\wedge j={\mathrm{coe}}_1\left(k\right)\left(x\right)\right)$$
28	27 11	cab	$$class\left\{j|\exists k\in i\left({\mathrm{deg}}_1\left(r\right)\left(k\right)\le x\wedge j={\mathrm{coe}}_1\left(k\right)\left(x\right)\right)\right\}$$
29	9 10 28	cmpt	$$class\left(x\in {\mathbb{N}}_0⟼\left\{j|\exists k\in i\left({\mathrm{deg}}_1\left(r\right)\left(k\right)\le x\wedge j={\mathrm{coe}}_1\left(k\right)\left(x\right)\right)\right\}\right)$$
30	3 8 29	cmpt	$$class\left(i\in \mathrm{LIdeal}\left({\mathrm{Poly}}_1\left(r\right)\right)⟼\left(x\in {\mathbb{N}}_0⟼\left\{j|\exists k\in i\left({\mathrm{deg}}_1\left(r\right)\left(k\right)\le x\wedge j={\mathrm{coe}}_1\left(k\right)\left(x\right)\right)\right\}\right)\right)$$
31	1 2 30	cmpt	$$class\left(r\in \mathrm{V}⟼\left(i\in \mathrm{LIdeal}\left({\mathrm{Poly}}_1\left(r\right)\right)⟼\left(x\in {\mathbb{N}}_0⟼\left\{j|\exists k\in i\left({\mathrm{deg}}_1\left(r\right)\left(k\right)\le x\wedge j={\mathrm{coe}}_1\left(k\right)\left(x\right)\right)\right\}\right)\right)\right)$$
32	0 31	wceq	$$wff\mathrm{ldgIdlSeq}=\left(r\in \mathrm{V}⟼\left(i\in \mathrm{LIdeal}\left({\mathrm{Poly}}_1\left(r\right)\right)⟼\left(x\in {\mathbb{N}}_0⟼\left\{j|\exists k\in i\left({\mathrm{deg}}_1\left(r\right)\left(k\right)\le x\wedge j={\mathrm{coe}}_1\left(k\right)\left(x\right)\right)\right\}\right)\right)\right)$$