Definition df-ldgis 37692

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 37700. (Contributed by Stefan O'Rear, 31-Mar-2015.)

Assertion

Ref	Expression
df-ldgis	|- ldgIdlSeq = ( r e. _V |-> ( i e. (LIdeal ` (Poly1 ` r ) ) |-> ( x e. NN0 |-> { j | E. k e. i ( ( ( deg1 ` r ) ` k ) <_ x /\ j = ( (coe1 ` k ) ` x ) ) } ) ) )

Distinct variable group:   i, r, x, j, k

Detailed syntax breakdown of Definition df-ldgis

Step	Hyp	Ref	Expression
1		cldgis 37691	. 2 class ldgIdlSeq
2		vr	. . 3 setvar r
3		cvv 3200	. . 3 class _V
4		vi	. . . 4 setvar i
5	2	cv 1482	. . . . . 6 class r
6		cpl1 19547	. . . . . 6 class Poly1
7	5, 6	cfv 5888	. . . . 5 class (Poly1 ` r )
8		clidl 19170	. . . . 5 class LIdeal
9	7, 8	cfv 5888	. . . 4 class (LIdeal ` (Poly1 ` r ) )
10		vx	. . . . 5 setvar x
11		cn0 11292	. . . . 5 class NN0
12		vk	. . . . . . . . . . 11 setvar k
13	12	cv 1482	. . . . . . . . . 10 class k
14		cdg1 23814	. . . . . . . . . . 11 class deg1
15	5, 14	cfv 5888	. . . . . . . . . 10 class ( deg1 ` r )
16	13, 15	cfv 5888	. . . . . . . . 9 class ( ( deg1 ` r ) ` k )
17	10	cv 1482	. . . . . . . . 9 class x
18		cle 10075	. . . . . . . . 9 class <_
19	16, 17, 18	wbr 4653	. . . . . . . 8 wff ( ( deg1 ` r ) ` k ) <_ x
20		vj	. . . . . . . . . 10 setvar j
21	20	cv 1482	. . . . . . . . 9 class j
22		cco1 19548	. . . . . . . . . . 11 class coe1
23	13, 22	cfv 5888	. . . . . . . . . 10 class (coe1 ` k )
24	17, 23	cfv 5888	. . . . . . . . 9 class ( (coe1 ` k ) ` x )
25	21, 24	wceq 1483	. . . . . . . 8 wff j = ( (coe1 ` k ) ` x )
26	19, 25	wa 384	. . . . . . 7 wff ( ( ( deg1 ` r ) ` k ) <_ x /\ j = ( (coe1 ` k ) ` x ) )
27	4	cv 1482	. . . . . . 7 class i
28	26, 12, 27	wrex 2913	. . . . . 6 wff E. k e. i ( ( ( deg1 ` r ) ` k ) <_ x /\ j = ( (coe1 ` k ) ` x ) )
29	28, 20	cab 2608	. . . . 5 class { j | E. k e. i ( ( ( deg1 ` r ) ` k ) <_ x /\ j = ( (coe1 ` k ) ` x ) ) }
30	10, 11, 29	cmpt 4729	. . . 4 class ( x e. NN0 |-> { j | E. k e. i ( ( ( deg1 ` r ) ` k ) <_ x /\ j = ( (coe1 ` k ) ` x ) ) } )
31	4, 9, 30	cmpt 4729	. . 3 class ( i e. (LIdeal ` (Poly1 ` r ) ) |-> ( x e. NN0 |-> { j | E. k e. i ( ( ( deg1 ` r ) ` k ) <_ x /\ j = ( (coe1 ` k ) ` x ) ) } ) )
32	2, 3, 31	cmpt 4729	. 2 class ( r e. _V |-> ( i e. (LIdeal ` (Poly1 ` r ) ) |-> ( x e. NN0 |-> { j | E. k e. i ( ( ( deg1 ` r ) ` k ) <_ x /\ j = ( (coe1 ` k ) ` x ) ) } ) ) )
33	1, 32	wceq 1483	1 wff ldgIdlSeq = ( r e. _V |-> ( i e. (LIdeal ` (Poly1 ` r ) ) |-> ( x e. NN0 |-> { j | E. k e. i ( ( ( deg1 ` r ) ` k ) <_ x /\ j = ( (coe1 ` k ) ` x ) ) } ) ) )

This definition is referenced by:  hbtlem1  37693  hbtlem7  37695