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

Definition df-ig1p 21724
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 21719 . 2  class idlGen1p
2 vr . . 3  setvar  r
3 cvv 3070 . . 3  class  _V
4 vi . . . 4  setvar  i
52cv 1369 . . . . . 6  class  r
6 cpl1 17742 . . . . . 6  class Poly1
75, 6cfv 5518 . . . . 5  class  (Poly1 `  r
)
8 clidl 17359 . . . . 5  class LIdeal
97, 8cfv 5518 . . . 4  class  (LIdeal `  (Poly1 `  r ) )
104cv 1369 . . . . . 6  class  i
11 c0g 14482 . . . . . . . 8  class  0g
127, 11cfv 5518 . . . . . . 7  class  ( 0g
`  (Poly1 `  r ) )
1312csn 3977 . . . . . 6  class  { ( 0g `  (Poly1 `  r
) ) }
1410, 13wceq 1370 . . . . 5  wff  i  =  { ( 0g `  (Poly1 `  r ) ) }
15 vg . . . . . . . . 9  setvar  g
1615cv 1369 . . . . . . . 8  class  g
17 cdg1 21641 . . . . . . . . 9  class deg1
185, 17cfv 5518 . . . . . . . 8  class  ( deg1  `  r
)
1916, 18cfv 5518 . . . . . . 7  class  ( ( deg1  `  r ) `  g
)
2010, 13cdif 3425 . . . . . . . . 9  class  ( i 
\  { ( 0g
`  (Poly1 `  r ) ) } )
2118, 20cima 4943 . . . . . . . 8  class  ( ( deg1  `  r ) " (
i  \  { ( 0g `  (Poly1 `  r ) ) } ) )
22 cr 9384 . . . . . . . 8  class  RR
23 clt 9521 . . . . . . . . 9  class  <
2423ccnv 4939 . . . . . . . 8  class  `'  <
2521, 22, 24csup 7793 . . . . . . 7  class  sup (
( ( deg1  `  r ) " ( i  \  { ( 0g `  (Poly1 `  r ) ) } ) ) ,  RR ,  `'  <  )
2619, 25wceq 1370 . . . . . 6  wff  ( ( deg1  `  r ) `  g
)  =  sup (
( ( deg1  `  r ) " ( i  \  { ( 0g `  (Poly1 `  r ) ) } ) ) ,  RR ,  `'  <  )
27 cmn1 21715 . . . . . . . 8  class Monic1p
285, 27cfv 5518 . . . . . . 7  class  (Monic1p `  r
)
2910, 28cin 3427 . . . . . 6  class  ( i  i^i  (Monic1p `  r ) )
3026, 15, 29crio 6152 . . . . 5  class  ( iota_ g  e.  ( i  i^i  (Monic1p `  r ) ) ( ( deg1  `  r ) `  g )  =  sup ( ( ( deg1  `  r
) " ( i 
\  { ( 0g
`  (Poly1 `  r ) ) } ) ) ,  RR ,  `'  <  ) )
3114, 12, 30cif 3891 . . . 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 4450 . . 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 4450 . 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 1370 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 setvar class
This definition is referenced by:  ig1pval  21762
  Copyright terms: Public domain W3C validator