MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ig1p Unicode version

Definition df-ig1p 19520
Description: Define a choice function for generators of ideals over a division ring; this is the unique monic polynomial of minimal degree in the ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.)
Assertion
Ref Expression
df-ig1p  |- idlGen1p  =  ( r  e.  _V  |->  ( i  e.  (LIdeal `  (Poly1 `  r
) )  |->  if ( i  =  { ( 0g `  (Poly1 `  r
) ) } , 
( 0g `  (Poly1 `  r ) ) ,  ( iota_ g  e.  ( i  i^i  (Monic1p `  r
) ) ( ( deg1  `  r ) `  g
)  =  sup (
( ( deg1  `  r ) " ( i  \  { ( 0g `  (Poly1 `  r ) ) } ) ) ,  RR ,  `'  <  ) ) ) ) )
Distinct variable group:    g, r, i

Detailed syntax breakdown of Definition df-ig1p
StepHypRef Expression
1 cig1p 19515 . 2  class idlGen1p
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 ) )
104cv 1622 . . . . . 6  class  i
11 c0g 13400 . . . . . . . 8  class  0g
127, 11cfv 5255 . . . . . . 7  class  ( 0g
`  (Poly1 `  r ) )
1312csn 3640 . . . . . 6  class  { ( 0g `  (Poly1 `  r
) ) }
1410, 13wceq 1623 . . . . 5  wff  i  =  { ( 0g `  (Poly1 `  r ) ) }
15 vg . . . . . . . . 9  set  g
1615cv 1622 . . . . . . . 8  class  g
17 cdg1 19440 . . . . . . . . 9  class deg1
185, 17cfv 5255 . . . . . . . 8  class  ( deg1  `  r
)
1916, 18cfv 5255 . . . . . . 7  class  ( ( deg1  `  r ) `  g
)
2010, 13cdif 3149 . . . . . . . . 9  class  ( i 
\  { ( 0g
`  (Poly1 `  r ) ) } )
2118, 20cima 4692 . . . . . . . 8  class  ( ( deg1  `  r ) " (
i  \  { ( 0g `  (Poly1 `  r ) ) } ) )
22 cr 8736 . . . . . . . 8  class  RR
23 clt 8867 . . . . . . . . 9  class  <
2423ccnv 4688 . . . . . . . 8  class  `'  <
2521, 22, 24csup 7193 . . . . . . 7  class  sup (
( ( deg1  `  r ) " ( i  \  { ( 0g `  (Poly1 `  r ) ) } ) ) ,  RR ,  `'  <  )
2619, 25wceq 1623 . . . . . 6  wff  ( ( deg1  `  r ) `  g
)  =  sup (
( ( deg1  `  r ) " ( i  \  { ( 0g `  (Poly1 `  r ) ) } ) ) ,  RR ,  `'  <  )
27 cmn1 19511 . . . . . . . 8  class Monic1p
285, 27cfv 5255 . . . . . . 7  class  (Monic1p `  r
)
2910, 28cin 3151 . . . . . 6  class  ( i  i^i  (Monic1p `  r ) )
3026, 15, 29crio 6297 . . . . 5  class  ( iota_ g  e.  ( i  i^i  (Monic1p `  r ) ) ( ( deg1  `  r ) `  g )  =  sup ( ( ( deg1  `  r
) " ( i 
\  { ( 0g
`  (Poly1 `  r ) ) } ) ) ,  RR ,  `'  <  ) )
3114, 12, 30cif 3565 . . . 4  class  if ( i  =  { ( 0g `  (Poly1 `  r
) ) } , 
( 0g `  (Poly1 `  r ) ) ,  ( iota_ g  e.  ( i  i^i  (Monic1p `  r
) ) ( ( deg1  `  r ) `  g
)  =  sup (
( ( deg1  `  r ) " ( i  \  { ( 0g `  (Poly1 `  r ) ) } ) ) ,  RR ,  `'  <  ) ) )
324, 9, 31cmpt 4077 . . 3  class  ( i  e.  (LIdeal `  (Poly1 `  r ) )  |->  if ( i  =  {
( 0g `  (Poly1 `  r ) ) } ,  ( 0g `  (Poly1 `  r ) ) ,  ( iota_ g  e.  ( i  i^i  (Monic1p `  r
) ) ( ( deg1  `  r ) `  g
)  =  sup (
( ( deg1  `  r ) " ( i  \  { ( 0g `  (Poly1 `  r ) ) } ) ) ,  RR ,  `'  <  ) ) ) )
332, 3, 32cmpt 4077 . 2  class  ( r  e.  _V  |->  ( i  e.  (LIdeal `  (Poly1 `  r ) )  |->  if ( i  =  {
( 0g `  (Poly1 `  r ) ) } ,  ( 0g `  (Poly1 `  r ) ) ,  ( iota_ g  e.  ( i  i^i  (Monic1p `  r
) ) ( ( deg1  `  r ) `  g
)  =  sup (
( ( deg1  `  r ) " ( i  \  { ( 0g `  (Poly1 `  r ) ) } ) ) ,  RR ,  `'  <  ) ) ) ) )
341, 33wceq 1623 1  wff idlGen1p  =  ( r  e.  _V  |->  ( i  e.  (LIdeal `  (Poly1 `  r
) )  |->  if ( i  =  { ( 0g `  (Poly1 `  r
) ) } , 
( 0g `  (Poly1 `  r ) ) ,  ( iota_ g  e.  ( i  i^i  (Monic1p `  r
) ) ( ( deg1  `  r ) `  g
)  =  sup (
( ( deg1  `  r ) " ( i  \  { ( 0g `  (Poly1 `  r ) ) } ) ) ,  RR ,  `'  <  ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  ig1pval  19558
  Copyright terms: Public domain W3C validator