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

Definition df-ldgis 27326
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 27334. (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
StepHypRef Expression
1 cldgis 27325 . 2  class ldgIdlSeq
2 vr . . 3  set  r
3 cvv 2788 . . 3  class  _V
4 vi . . . 4  set  i
52cv 1622 . . . . . 6  class  r
6 cpl1 16252 . . . . . 6  class Poly1
75, 6cfv 5255 . . . . 5  class  (Poly1 `  r
)
8 clidl 15923 . . . . 5  class LIdeal
97, 8cfv 5255 . . . 4  class  (LIdeal `  (Poly1 `  r ) )
10 vx . . . . 5  set  x
11 cn0 9965 . . . . 5  class  NN0
12 vk . . . . . . . . . . 11  set  k
1312cv 1622 . . . . . . . . . 10  class  k
14 cdg1 19440 . . . . . . . . . . 11  class deg1
155, 14cfv 5255 . . . . . . . . . 10  class  ( deg1  `  r
)
1613, 15cfv 5255 . . . . . . . . 9  class  ( ( deg1  `  r ) `  k
)
1710cv 1622 . . . . . . . . 9  class  x
18 cle 8868 . . . . . . . . 9  class  <_
1916, 17, 18wbr 4023 . . . . . . . 8  wff  ( ( deg1  `  r ) `  k
)  <_  x
20 vj . . . . . . . . . 10  set  j
2120cv 1622 . . . . . . . . 9  class  j
22 cco1 16255 . . . . . . . . . . 11  class coe1
2313, 22cfv 5255 . . . . . . . . . 10  class  (coe1 `  k
)
2417, 23cfv 5255 . . . . . . . . 9  class  ( (coe1 `  k ) `  x
)
2521, 24wceq 1623 . . . . . . . 8  wff  j  =  ( (coe1 `  k ) `  x )
2619, 25wa 358 . . . . . . 7  wff  ( ( ( deg1  `  r ) `  k )  <_  x  /\  j  =  (
(coe1 `  k ) `  x ) )
274cv 1622 . . . . . . 7  class  i
2826, 12, 27wrex 2544 . . . . . 6  wff  E. k  e.  i  ( (
( deg1  `
 r ) `  k )  <_  x  /\  j  =  (
(coe1 `  k ) `  x ) )
2928, 20cab 2269 . . . . 5  class  { j  |  E. k  e.  i  ( ( ( deg1  `  r ) `  k
)  <_  x  /\  j  =  ( (coe1 `  k ) `  x
) ) }
3010, 11, 29cmpt 4077 . . . 4  class  ( x  e.  NN0  |->  { j  |  E. k  e.  i  ( ( ( deg1  `  r ) `  k
)  <_  x  /\  j  =  ( (coe1 `  k ) `  x
) ) } )
314, 9, 30cmpt 4077 . . 3  class  ( i  e.  (LIdeal `  (Poly1 `  r ) )  |->  ( x  e.  NN0  |->  { j  |  E. k  e.  i  ( ( ( deg1  `  r ) `  k
)  <_  x  /\  j  =  ( (coe1 `  k ) `  x
) ) } ) )
322, 3, 31cmpt 4077 . 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
) ) } ) ) )
331, 32wceq 1623 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
) ) } ) ) )
Colors of variables: wff set class
This definition is referenced by:  hbtlem1  27327  hbtlem7  27329
  Copyright terms: Public domain W3C validator