Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ldgis Structured version   Unicode version

Definition df-ldgis 27303
 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 27311. (Contributed by Stefan O'Rear, 31-Mar-2015.)
Assertion
Ref Expression
df-ldgis ldgIdlSeq LIdealPoly1 deg1 coe1
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-ldgis
StepHypRef Expression
1 cldgis 27302 . 2 ldgIdlSeq
2 vr . . 3
3 cvv 2956 . . 3
4 vi . . . 4
52cv 1651 . . . . . 6
6 cpl1 16571 . . . . . 6 Poly1
75, 6cfv 5454 . . . . 5 Poly1
8 clidl 16242 . . . . 5 LIdeal
97, 8cfv 5454 . . . 4 LIdealPoly1
10 vx . . . . 5
11 cn0 10221 . . . . 5
12 vk . . . . . . . . . . 11
1312cv 1651 . . . . . . . . . 10
14 cdg1 19977 . . . . . . . . . . 11 deg1
155, 14cfv 5454 . . . . . . . . . 10 deg1
1613, 15cfv 5454 . . . . . . . . 9 deg1
1710cv 1651 . . . . . . . . 9
18 cle 9121 . . . . . . . . 9
1916, 17, 18wbr 4212 . . . . . . . 8 deg1
20 vj . . . . . . . . . 10
2120cv 1651 . . . . . . . . 9
22 cco1 16574 . . . . . . . . . . 11 coe1
2313, 22cfv 5454 . . . . . . . . . 10 coe1
2417, 23cfv 5454 . . . . . . . . 9 coe1
2521, 24wceq 1652 . . . . . . . 8 coe1
2619, 25wa 359 . . . . . . 7 deg1 coe1
274cv 1651 . . . . . . 7
2826, 12, 27wrex 2706 . . . . . 6 deg1 coe1
2928, 20cab 2422 . . . . 5 deg1 coe1
3010, 11, 29cmpt 4266 . . . 4 deg1 coe1
314, 9, 30cmpt 4266 . . 3 LIdealPoly1 deg1 coe1
322, 3, 31cmpt 4266 . 2 LIdealPoly1 deg1 coe1
331, 32wceq 1652 1 ldgIdlSeq LIdealPoly1 deg1 coe1
 Colors of variables: wff set class This definition is referenced by:  hbtlem1  27304  hbtlem7  27306
 Copyright terms: Public domain W3C validator