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

Definition df-sfl1 25075
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 25067 . 2  class splitFld1
2 vr . . 3  set  r
3 vj . . 3  set  j
4 cvv 2956 . . 3  class  _V
5 vp . . . 4  set  p
62cv 1651 . . . . 5  class  r
7 cpl1 16571 . . . . 5  class Poly1
86, 7cfv 5454 . . . 4  class  (Poly1 `  r
)
9 c1 8991 . . . . . . 7  class  1
105cv 1651 . . . . . . . 8  class  p
11 cdg1 19977 . . . . . . . 8  class deg1
126, 10, 11co 6081 . . . . . . 7  class  ( r deg1  p )
13 cfz 11043 . . . . . . 7  class  ...
149, 12, 13co 6081 . . . . . 6  class  ( 1 ... ( r deg1  p ) )
15 ccrd 7822 . . . . . 6  class  card
1614, 15cfv 5454 . . . . 5  class  ( card `  ( 1 ... (
r deg1  p ) ) )
17 vs . . . . . . 7  set  s
18 vf . . . . . . 7  set  f
19 vm . . . . . . . 8  set  m
2017cv 1651 . . . . . . . . 9  class  s
21 cmpl 16408 . . . . . . . . 9  class mPoly
2220, 21cfv 5454 . . . . . . . 8  class  ( mPoly  `  s
)
23 vb . . . . . . . . 9  set  b
24 vg . . . . . . . . . . . . 13  set  g
2524cv 1651 . . . . . . . . . . . 12  class  g
2618cv 1651 . . . . . . . . . . . . 13  class  f
2710, 26ccom 4882 . . . . . . . . . . . 12  class  ( p  o.  f )
2819cv 1651 . . . . . . . . . . . . 13  class  m
29 cdsr 15743 . . . . . . . . . . . . 13  class  ||r
3028, 29cfv 5454 . . . . . . . . . . . 12  class  ( ||r `  m
)
3125, 27, 30wbr 4212 . . . . . . . . . . 11  wff  g (
||r `  m ) ( p  o.  f )
3220, 25, 11co 6081 . . . . . . . . . . . 12  class  ( s deg1  g )
33 clt 9120 . . . . . . . . . . . 12  class  <
349, 32, 33wbr 4212 . . . . . . . . . . 11  wff  1  <  ( s deg1  g )
3531, 34wa 359 . . . . . . . . . 10  wff  ( g ( ||r `
 m ) ( p  o.  f )  /\  1  <  (
s deg1  g ) )
36 cmn1 20048 . . . . . . . . . . . 12  class Monic1p
3720, 36cfv 5454 . . . . . . . . . . 11  class  (Monic1p `  s
)
38 cir 15745 . . . . . . . . . . . 12  class Irred
3928, 38cfv 5454 . . . . . . . . . . 11  class  (Irred `  m )
4037, 39cin 3319 . . . . . . . . . 10  class  ( (Monic1p `  s )  i^i  (Irred `  m ) )
4135, 24, 40crab 2709 . . . . . . . . 9  class  { g  e.  ( (Monic1p `  s
)  i^i  (Irred `  m
) )  |  ( g ( ||r `
 m ) ( p  o.  f )  /\  1  <  (
s deg1  g ) ) }
42 c0g 13723 . . . . . . . . . . . . 13  class  0g
4328, 42cfv 5454 . . . . . . . . . . . 12  class  ( 0g
`  m )
4427, 43wceq 1652 . . . . . . . . . . 11  wff  ( p  o.  f )  =  ( 0g `  m
)
4523cv 1651 . . . . . . . . . . . 12  class  b
46 c0 3628 . . . . . . . . . . . 12  class  (/)
4745, 46wceq 1652 . . . . . . . . . . 11  wff  b  =  (/)
4844, 47wo 358 . . . . . . . . . 10  wff  ( ( p  o.  f )  =  ( 0g `  m )  \/  b  =  (/) )
4920, 26cop 3817 . . . . . . . . . 10  class  <. s ,  f >.
50 vh . . . . . . . . . . 11  set  h
51 cglb 14400 . . . . . . . . . . . 12  class  glb
5245, 51cfv 5454 . . . . . . . . . . 11  class  ( glb `  b )
53 vt . . . . . . . . . . . 12  set  t
5450cv 1651 . . . . . . . . . . . . 13  class  h
55 cpfl 25066 . . . . . . . . . . . . 13  class polyFld
5620, 54, 55co 6081 . . . . . . . . . . . 12  class  ( s polyFld  h )
5753cv 1651 . . . . . . . . . . . . . 14  class  t
58 c1st 6347 . . . . . . . . . . . . . 14  class  1st
5957, 58cfv 5454 . . . . . . . . . . . . 13  class  ( 1st `  t )
60 c2nd 6348 . . . . . . . . . . . . . . 15  class  2nd
6157, 60cfv 5454 . . . . . . . . . . . . . 14  class  ( 2nd `  t )
6226, 61ccom 4882 . . . . . . . . . . . . 13  class  ( f  o.  ( 2nd `  t
) )
6359, 62cop 3817 . . . . . . . . . . . 12  class  <. ( 1st `  t ) ,  ( f  o.  ( 2nd `  t ) )
>.
6453, 56, 63csb 3251 . . . . . . . . . . 11  class  [_ (
s polyFld  h )  /  t ]_ <. ( 1st `  t
) ,  ( f  o.  ( 2nd `  t
) ) >.
6550, 52, 64csb 3251 . . . . . . . . . 10  class  [_ ( glb `  b )  /  h ]_ [_ ( s polyFld  h )  /  t ]_ <. ( 1st `  t
) ,  ( f  o.  ( 2nd `  t
) ) >.
6648, 49, 65cif 3739 . . . . . . . . 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 3251 . . . . . . . 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 3251 . . . . . . 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 6083 . . . . . 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 1651 . . . . . 6  class  j
7169, 70crdg 6667 . . . . 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 5454 . . . 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 4266 . . 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 6083 . 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 1652 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