Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sfl1 Unicode version

Definition df-sfl1 23986
Description: Temporary construction for the splitting field of a polynomial. The inputs are a field  r and a polynomial  p that we want to split, along with a tuple  j in the same format as the output. The output is a tuple  <. S ,  F >. where 
S is the splitting field and  F is an injective homomorphism from the original field  r.

The function works by repeatedly finding the smallest monic irreducible factor, and extending the field by that factor using the polyFld construction. We keep track of a total order in each of the splitting fields so that we can pick an element definably without needing global choice. (Contributed by Mario Carneiro, 2-Dec-2014.)

Assertion
Ref Expression
df-sfl1  |- splitFld1  =  ( r  e.  _V ,  j  e. 
_V  |->  ( p  e.  (Poly1 `  r )  |->  ( rec ( ( s  e.  _V ,  f  e.  _V  |->  [_ ( mPoly  `  s )  /  m ]_ [_ { g  e.  ( (Monic1p `  s )  i^i  (Irred `  m )
)  |  ( g ( ||r `
 m ) ( p  o.  f )  /\  1  <  (
s deg1  g ) ) }  /  b ]_ if ( ( ( p  o.  f )  =  ( 0g `  m
)  \/  b  =  (/) ) ,  <. s ,  f >. ,  [_ ( glb `  b )  /  h ]_ [_ (
s polyFld  h )  /  t ]_ <. ( 1st `  t
) ,  ( f  o.  ( 2nd `  t
) ) >. )
) ,  j ) `
 ( card `  (
1 ... ( r deg1  p ) ) ) ) ) )
Distinct variable group:    f, b, g, h, j, m, p, r, s, t

Detailed syntax breakdown of Definition df-sfl1
StepHypRef Expression
1 csf1 23978 . 2  class splitFld1
2 vr . . 3  set  r
3 vj . . 3  set  j
4 cvv 2801 . . 3  class  _V
5 vp . . . 4  set  p
62cv 1631 . . . . 5  class  r
7 cpl1 16268 . . . . 5  class Poly1
86, 7cfv 5271 . . . 4  class  (Poly1 `  r
)
9 c1 8754 . . . . . . 7  class  1
105cv 1631 . . . . . . . 8  class  p
11 cdg1 19456 . . . . . . . 8  class deg1
126, 10, 11co 5874 . . . . . . 7  class  ( r deg1  p )
13 cfz 10798 . . . . . . 7  class  ...
149, 12, 13co 5874 . . . . . 6  class  ( 1 ... ( r deg1  p ) )
15 ccrd 7584 . . . . . 6  class  card
1614, 15cfv 5271 . . . . 5  class  ( card `  ( 1 ... (
r deg1  p ) ) )
17 vs . . . . . . 7  set  s
18 vf . . . . . . 7  set  f
19 vm . . . . . . . 8  set  m
2017cv 1631 . . . . . . . . 9  class  s
21 cmpl 16105 . . . . . . . . 9  class mPoly
2220, 21cfv 5271 . . . . . . . 8  class  ( mPoly  `  s
)
23 vb . . . . . . . . 9  set  b
24 vg . . . . . . . . . . . . 13  set  g
2524cv 1631 . . . . . . . . . . . 12  class  g
2618cv 1631 . . . . . . . . . . . . 13  class  f
2710, 26ccom 4709 . . . . . . . . . . . 12  class  ( p  o.  f )
2819cv 1631 . . . . . . . . . . . . 13  class  m
29 cdsr 15436 . . . . . . . . . . . . 13  class  ||r
3028, 29cfv 5271 . . . . . . . . . . . 12  class  ( ||r `  m
)
3125, 27, 30wbr 4039 . . . . . . . . . . 11  wff  g (
||r `  m ) ( p  o.  f )
3220, 25, 11co 5874 . . . . . . . . . . . 12  class  ( s deg1  g )
33 clt 8883 . . . . . . . . . . . 12  class  <
349, 32, 33wbr 4039 . . . . . . . . . . 11  wff  1  <  ( s deg1  g )
3531, 34wa 358 . . . . . . . . . 10  wff  ( g ( ||r `
 m ) ( p  o.  f )  /\  1  <  (
s deg1  g ) )
36 cmn1 19527 . . . . . . . . . . . 12  class Monic1p
3720, 36cfv 5271 . . . . . . . . . . 11  class  (Monic1p `  s
)
38 cir 15438 . . . . . . . . . . . 12  class Irred
3928, 38cfv 5271 . . . . . . . . . . 11  class  (Irred `  m )
4037, 39cin 3164 . . . . . . . . . 10  class  ( (Monic1p `  s )  i^i  (Irred `  m ) )
4135, 24, 40crab 2560 . . . . . . . . 9  class  { g  e.  ( (Monic1p `  s
)  i^i  (Irred `  m
) )  |  ( g ( ||r `
 m ) ( p  o.  f )  /\  1  <  (
s deg1  g ) ) }
42 c0g 13416 . . . . . . . . . . . . 13  class  0g
4328, 42cfv 5271 . . . . . . . . . . . 12  class  ( 0g
`  m )
4427, 43wceq 1632 . . . . . . . . . . 11  wff  ( p  o.  f )  =  ( 0g `  m
)
4523cv 1631 . . . . . . . . . . . 12  class  b
46 c0 3468 . . . . . . . . . . . 12  class  (/)
4745, 46wceq 1632 . . . . . . . . . . 11  wff  b  =  (/)
4844, 47wo 357 . . . . . . . . . 10  wff  ( ( p  o.  f )  =  ( 0g `  m )  \/  b  =  (/) )
4920, 26cop 3656 . . . . . . . . . 10  class  <. s ,  f >.
50 vh . . . . . . . . . . 11  set  h
51 cglb 14093 . . . . . . . . . . . 12  class  glb
5245, 51cfv 5271 . . . . . . . . . . 11  class  ( glb `  b )
53 vt . . . . . . . . . . . 12  set  t
5450cv 1631 . . . . . . . . . . . . 13  class  h
55 cpfl 23977 . . . . . . . . . . . . 13  class polyFld
5620, 54, 55co 5874 . . . . . . . . . . . 12  class  ( s polyFld  h )
5753cv 1631 . . . . . . . . . . . . . 14  class  t
58 c1st 6136 . . . . . . . . . . . . . 14  class  1st
5957, 58cfv 5271 . . . . . . . . . . . . 13  class  ( 1st `  t )
60 c2nd 6137 . . . . . . . . . . . . . . 15  class  2nd
6157, 60cfv 5271 . . . . . . . . . . . . . 14  class  ( 2nd `  t )
6226, 61ccom 4709 . . . . . . . . . . . . 13  class  ( f  o.  ( 2nd `  t
) )
6359, 62cop 3656 . . . . . . . . . . . 12  class  <. ( 1st `  t ) ,  ( f  o.  ( 2nd `  t ) )
>.
6453, 56, 63csb 3094 . . . . . . . . . . 11  class  [_ (
s polyFld  h )  /  t ]_ <. ( 1st `  t
) ,  ( f  o.  ( 2nd `  t
) ) >.
6550, 52, 64csb 3094 . . . . . . . . . 10  class  [_ ( glb `  b )  /  h ]_ [_ ( s polyFld  h )  /  t ]_ <. ( 1st `  t
) ,  ( f  o.  ( 2nd `  t
) ) >.
6648, 49, 65cif 3578 . . . . . . . . 9  class  if ( ( ( p  o.  f )  =  ( 0g `  m )  \/  b  =  (/) ) ,  <. s ,  f >. ,  [_ ( glb `  b )  /  h ]_ [_ ( s polyFld  h )  /  t ]_ <. ( 1st `  t
) ,  ( f  o.  ( 2nd `  t
) ) >. )
6723, 41, 66csb 3094 . . . . . . . 8  class  [_ {
g  e.  ( (Monic1p `  s )  i^i  (Irred `  m ) )  |  ( g ( ||r `  m
) ( p  o.  f )  /\  1  <  ( s deg1  g ) ) }  /  b ]_ if ( ( ( p  o.  f )  =  ( 0g `  m
)  \/  b  =  (/) ) ,  <. s ,  f >. ,  [_ ( glb `  b )  /  h ]_ [_ (
s polyFld  h )  /  t ]_ <. ( 1st `  t
) ,  ( f  o.  ( 2nd `  t
) ) >. )
6819, 22, 67csb 3094 . . . . . . 7  class  [_ ( mPoly  `  s )  /  m ]_ [_ { g  e.  ( (Monic1p `  s )  i^i  (Irred `  m )
)  |  ( g ( ||r `
 m ) ( p  o.  f )  /\  1  <  (
s deg1  g ) ) }  /  b ]_ if ( ( ( p  o.  f )  =  ( 0g `  m
)  \/  b  =  (/) ) ,  <. s ,  f >. ,  [_ ( glb `  b )  /  h ]_ [_ (
s polyFld  h )  /  t ]_ <. ( 1st `  t
) ,  ( f  o.  ( 2nd `  t
) ) >. )
6917, 18, 4, 4, 68cmpt2 5876 . . . . . 6  class  ( s  e.  _V ,  f  e.  _V  |->  [_ ( mPoly  `  s )  /  m ]_ [_ { g  e.  ( (Monic1p `  s )  i^i  (Irred `  m )
)  |  ( g ( ||r `
 m ) ( p  o.  f )  /\  1  <  (
s deg1  g ) ) }  /  b ]_ if ( ( ( p  o.  f )  =  ( 0g `  m
)  \/  b  =  (/) ) ,  <. s ,  f >. ,  [_ ( glb `  b )  /  h ]_ [_ (
s polyFld  h )  /  t ]_ <. ( 1st `  t
) ,  ( f  o.  ( 2nd `  t
) ) >. )
)
703cv 1631 . . . . . 6  class  j
7169, 70crdg 6438 . . . . 5  class  rec (
( s  e.  _V ,  f  e.  _V  |->  [_ ( mPoly  `  s )  /  m ]_ [_ {
g  e.  ( (Monic1p `  s )  i^i  (Irred `  m ) )  |  ( g ( ||r `  m
) ( p  o.  f )  /\  1  <  ( s deg1  g ) ) }  /  b ]_ if ( ( ( p  o.  f )  =  ( 0g `  m
)  \/  b  =  (/) ) ,  <. s ,  f >. ,  [_ ( glb `  b )  /  h ]_ [_ (
s polyFld  h )  /  t ]_ <. ( 1st `  t
) ,  ( f  o.  ( 2nd `  t
) ) >. )
) ,  j )
7216, 71cfv 5271 . . . 4  class  ( rec ( ( s  e. 
_V ,  f  e. 
_V  |->  [_ ( mPoly  `  s
)  /  m ]_ [_ { g  e.  ( (Monic1p `  s )  i^i  (Irred `  m )
)  |  ( g ( ||r `
 m ) ( p  o.  f )  /\  1  <  (
s deg1  g ) ) }  /  b ]_ if ( ( ( p  o.  f )  =  ( 0g `  m
)  \/  b  =  (/) ) ,  <. s ,  f >. ,  [_ ( glb `  b )  /  h ]_ [_ (
s polyFld  h )  /  t ]_ <. ( 1st `  t
) ,  ( f  o.  ( 2nd `  t
) ) >. )
) ,  j ) `
 ( card `  (
1 ... ( r deg1  p ) ) ) )
735, 8, 72cmpt 4093 . . 3  class  ( p  e.  (Poly1 `  r )  |->  ( rec ( ( s  e.  _V ,  f  e.  _V  |->  [_ ( mPoly  `  s )  /  m ]_ [_ { g  e.  ( (Monic1p `  s )  i^i  (Irred `  m )
)  |  ( g ( ||r `
 m ) ( p  o.  f )  /\  1  <  (
s deg1  g ) ) }  /  b ]_ if ( ( ( p  o.  f )  =  ( 0g `  m
)  \/  b  =  (/) ) ,  <. s ,  f >. ,  [_ ( glb `  b )  /  h ]_ [_ (
s polyFld  h )  /  t ]_ <. ( 1st `  t
) ,  ( f  o.  ( 2nd `  t
) ) >. )
) ,  j ) `
 ( card `  (
1 ... ( r deg1  p ) ) ) ) )
742, 3, 4, 4, 73cmpt2 5876 . 2  class  ( r  e.  _V ,  j  e.  _V  |->  ( p  e.  (Poly1 `  r )  |->  ( rec ( ( s  e.  _V ,  f  e.  _V  |->  [_ ( mPoly  `  s )  /  m ]_ [_ { g  e.  ( (Monic1p `  s )  i^i  (Irred `  m )
)  |  ( g ( ||r `
 m ) ( p  o.  f )  /\  1  <  (
s deg1  g ) ) }  /  b ]_ if ( ( ( p  o.  f )  =  ( 0g `  m
)  \/  b  =  (/) ) ,  <. s ,  f >. ,  [_ ( glb `  b )  /  h ]_ [_ (
s polyFld  h )  /  t ]_ <. ( 1st `  t
) ,  ( f  o.  ( 2nd `  t
) ) >. )
) ,  j ) `
 ( card `  (
1 ... ( r deg1  p ) ) ) ) ) )
751, 74wceq 1632 1  wff splitFld1  =  ( r  e.  _V ,  j  e. 
_V  |->  ( p  e.  (Poly1 `  r )  |->  ( rec ( ( s  e.  _V ,  f  e.  _V  |->  [_ ( mPoly  `  s )  /  m ]_ [_ { g  e.  ( (Monic1p `  s )  i^i  (Irred `  m )
)  |  ( g ( ||r `
 m ) ( p  o.  f )  /\  1  <  (
s deg1  g ) ) }  /  b ]_ if ( ( ( p  o.  f )  =  ( 0g `  m
)  \/  b  =  (/) ) ,  <. s ,  f >. ,  [_ ( glb `  b )  /  h ]_ [_ (
s polyFld  h )  /  t ]_ <. ( 1st `  t
) ,  ( f  o.  ( 2nd `  t
) ) >. )
) ,  j ) `
 ( card `  (
1 ... ( r deg1  p ) ) ) ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator