Users' Mathboxes 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 29504
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 29512. (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 29503 . 2  class ldgIdlSeq
2 vr . . 3  setvar  r
3 cvv 2993 . . 3  class  _V
4 vi . . . 4  setvar  i
52cv 1368 . . . . . 6  class  r
6 cpl1 17655 . . . . . 6  class Poly1
75, 6cfv 5439 . . . . 5  class  (Poly1 `  r
)
8 clidl 17273 . . . . 5  class LIdeal
97, 8cfv 5439 . . . 4  class  (LIdeal `  (Poly1 `  r ) )
10 vx . . . . 5  setvar  x
11 cn0 10600 . . . . 5  class  NN0
12 vk . . . . . . . . . . 11  setvar  k
1312cv 1368 . . . . . . . . . 10  class  k
14 cdg1 21545 . . . . . . . . . . 11  class deg1
155, 14cfv 5439 . . . . . . . . . 10  class  ( deg1  `  r
)
1613, 15cfv 5439 . . . . . . . . 9  class  ( ( deg1  `  r ) `  k
)
1710cv 1368 . . . . . . . . 9  class  x
18 cle 9440 . . . . . . . . 9  class  <_
1916, 17, 18wbr 4313 . . . . . . . 8  wff  ( ( deg1  `  r ) `  k
)  <_  x
20 vj . . . . . . . . . 10  setvar  j
2120cv 1368 . . . . . . . . 9  class  j
22 cco1 17656 . . . . . . . . . . 11  class coe1
2313, 22cfv 5439 . . . . . . . . . 10  class  (coe1 `  k
)
2417, 23cfv 5439 . . . . . . . . 9  class  ( (coe1 `  k ) `  x
)
2521, 24wceq 1369 . . . . . . . 8  wff  j  =  ( (coe1 `  k ) `  x )
2619, 25wa 369 . . . . . . 7  wff  ( ( ( deg1  `  r ) `  k )  <_  x  /\  j  =  (
(coe1 `  k ) `  x ) )
274cv 1368 . . . . . . 7  class  i
2826, 12, 27wrex 2737 . . . . . 6  wff  E. k  e.  i  ( (
( deg1  `
 r ) `  k )  <_  x  /\  j  =  (
(coe1 `  k ) `  x ) )
2928, 20cab 2429 . . . . 5  class  { j  |  E. k  e.  i  ( ( ( deg1  `  r ) `  k
)  <_  x  /\  j  =  ( (coe1 `  k ) `  x
) ) }
3010, 11, 29cmpt 4371 . . . 4  class  ( x  e.  NN0  |->  { j  |  E. k  e.  i  ( ( ( deg1  `  r ) `  k
)  <_  x  /\  j  =  ( (coe1 `  k ) `  x
) ) } )
314, 9, 30cmpt 4371 . . 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 4371 . 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 1369 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 setvar class
This definition is referenced by:  hbtlem1  29505  hbtlem7  29507
  Copyright terms: Public domain W3C validator