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	|- 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 ) ) } ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cldgis	|- ldgIdlSeq
1		vr	|- r
2		cvv	|- _V
3		vi	|- i
4		clidl	|- LIdeal
5		cpl1	|- Poly1
6	1	cv	|- r
7	6 5	cfv	|- ( Poly1 ` r )
8	7 4	cfv	|- ( LIdeal ` ( Poly1 ` r ) )
9		vx	|- x
10		cn0	|- NN0
11		vj	|- j
12		vk	|- k
13	3	cv	|- i
14		cdg1	|- deg1
15	6 14	cfv	|- ( deg1 ` r )
16	12	cv	|- k
17	16 15	cfv	|- ( ( deg1 ` r ) ` k )
18		cle	|- <_
19	9	cv	|- x
20	17 19 18	wbr	|- ( ( deg1 ` r ) ` k ) <_ x
21	11	cv	|- j
22		cco1	|- coe1
23	16 22	cfv	|- ( coe1 ` k )
24	19 23	cfv	|- ( ( coe1 ` k ) ` x )
25	21 24	wceq	|- j = ( ( coe1 ` k ) ` x )
26	20 25	wa	|- ( ( ( deg1 ` r ) ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) )
27	26 12 13	wrex	|- E. k e. i ( ( ( deg1 ` r ) ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) )
28	27 11	cab	|- { j | E. k e. i ( ( ( deg1 ` r ) ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) }
29	9 10 28	cmpt	|- ( x e. NN0 |-> { j | E. k e. i ( ( ( deg1 ` r ) ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } )
30	3 8 29	cmpt	|- ( i e. ( LIdeal ` ( Poly1 ` r ) ) |-> ( x e. NN0 |-> { j | E. k e. i ( ( ( deg1 ` r ) ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) )
31	1 2 30	cmpt	|- ( r e. _V |-> ( i e. ( LIdeal ` ( Poly1 ` r ) ) |-> ( x e. NN0 |-> { j | E. k e. i ( ( ( deg1 ` r ) ` k ) <_ x /\ j = ( ( coe1 ` k ) ` x ) ) } ) ) )
32	0 31	wceq	|- 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 ) ) } ) ) )