Metamath Proof Explorer


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 V i LIdeal Poly 1 r x 0 j | k i deg 1 r k x j = coe 1 k x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cldgis class ldgIdlSeq
1 vr setvar r
2 cvv class V
3 vi setvar i
4 clidl class LIdeal
5 cpl1 class Poly 1
6 1 cv setvar r
7 6 5 cfv class Poly 1 r
8 7 4 cfv class LIdeal Poly 1 r
9 vx setvar x
10 cn0 class 0
11 vj setvar j
12 vk setvar k
13 3 cv setvar i
14 cdg1 class deg 1
15 6 14 cfv class deg 1 r
16 12 cv setvar k
17 16 15 cfv class deg 1 r k
18 cle class
19 9 cv setvar x
20 17 19 18 wbr wff deg 1 r k x
21 11 cv setvar j
22 cco1 class coe 1
23 16 22 cfv class coe 1 k
24 19 23 cfv class coe 1 k x
25 21 24 wceq wff j = coe 1 k x
26 20 25 wa wff deg 1 r k x j = coe 1 k x
27 26 12 13 wrex wff k i deg 1 r k x j = coe 1 k x
28 27 11 cab class j | k i deg 1 r k x j = coe 1 k x
29 9 10 28 cmpt class x 0 j | k i deg 1 r k x j = coe 1 k x
30 3 8 29 cmpt class i LIdeal Poly 1 r x 0 j | k i deg 1 r k x j = coe 1 k x
31 1 2 30 cmpt class r V i LIdeal Poly 1 r x 0 j | k i deg 1 r k x j = coe 1 k x
32 0 31 wceq wff ldgIdlSeq = r V i LIdeal Poly 1 r x 0 j | k i deg 1 r k x j = coe 1 k x