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

Definition df-sfl 23972
Description: Define the splitting field of a finite collection of polynomials, given a total ordered base field. The output is a tuple  <. S ,  F >. where  S is the totally ordered splitting field and  F is an injective homomorphism from the original field  r. (Contributed by Mario Carneiro, 2-Dec-2014.)
Assertion
Ref Expression
df-sfl  |- splitFld  =  ( r  e.  _V ,  p  e.  _V  |->  ( iota
x E. f ( f  Isom  <  ,  ( lt `  r ) ( ( 1 ... ( # `  p
) ) ,  p
)  /\  x  =  (  seq  0 ( ( e  e.  _V , 
g  e.  _V  |->  ( ( r splitFld1  e ) `  g
) ) ,  ( f  u.  { <. 0 ,  <. r ,  (  _I  |`  ( Base `  r ) )
>. >. } ) ) `
 ( # `  p
) ) ) ) )
Distinct variable group:    e, f, g, p, r, x

Detailed syntax breakdown of Definition df-sfl
StepHypRef Expression
1 csf 23964 . 2  class splitFld
2 vr . . 3  set  r
3 vp . . 3  set  p
4 cvv 2788 . . 3  class  _V
5 c1 8738 . . . . . . . 8  class  1
63cv 1622 . . . . . . . . 9  class  p
7 chash 11337 . . . . . . . . 9  class  #
86, 7cfv 5255 . . . . . . . 8  class  ( # `  p )
9 cfz 10782 . . . . . . . 8  class  ...
105, 8, 9co 5858 . . . . . . 7  class  ( 1 ... ( # `  p
) )
11 clt 8867 . . . . . . 7  class  <
122cv 1622 . . . . . . . 8  class  r
13 cplt 14075 . . . . . . . 8  class  lt
1412, 13cfv 5255 . . . . . . 7  class  ( lt
`  r )
15 vf . . . . . . . 8  set  f
1615cv 1622 . . . . . . 7  class  f
1710, 6, 11, 14, 16wiso 5256 . . . . . 6  wff  f  Isom  <  ,  ( lt `  r ) ( ( 1 ... ( # `  p ) ) ,  p )
18 vx . . . . . . . 8  set  x
1918cv 1622 . . . . . . 7  class  x
20 ve . . . . . . . . . 10  set  e
21 vg . . . . . . . . . 10  set  g
2221cv 1622 . . . . . . . . . . 11  class  g
2320cv 1622 . . . . . . . . . . . 12  class  e
24 csf1 23963 . . . . . . . . . . . 12  class splitFld1
2512, 23, 24co 5858 . . . . . . . . . . 11  class  ( r splitFld1  e )
2622, 25cfv 5255 . . . . . . . . . 10  class  ( ( r splitFld1  e ) `  g
)
2720, 21, 4, 4, 26cmpt2 5860 . . . . . . . . 9  class  ( e  e.  _V ,  g  e.  _V  |->  ( ( r splitFld1  e ) `  g
) )
28 cc0 8737 . . . . . . . . . . . 12  class  0
29 cid 4304 . . . . . . . . . . . . . 14  class  _I
30 cbs 13148 . . . . . . . . . . . . . . 15  class  Base
3112, 30cfv 5255 . . . . . . . . . . . . . 14  class  ( Base `  r )
3229, 31cres 4691 . . . . . . . . . . . . 13  class  (  _I  |`  ( Base `  r
) )
3312, 32cop 3643 . . . . . . . . . . . 12  class  <. r ,  (  _I  |`  ( Base `  r ) )
>.
3428, 33cop 3643 . . . . . . . . . . 11  class  <. 0 ,  <. r ,  (  _I  |`  ( Base `  r ) ) >. >.
3534csn 3640 . . . . . . . . . 10  class  { <. 0 ,  <. r ,  (  _I  |`  ( Base `  r ) )
>. >. }
3616, 35cun 3150 . . . . . . . . 9  class  ( f  u.  { <. 0 ,  <. r ,  (  _I  |`  ( Base `  r ) ) >. >. } )
3727, 36, 28cseq 11046 . . . . . . . 8  class  seq  0
( ( e  e. 
_V ,  g  e. 
_V  |->  ( ( r splitFld1  e ) `  g ) ) ,  ( f  u.  { <. 0 ,  <. r ,  (  _I  |`  ( Base `  r ) ) >. >. } ) )
388, 37cfv 5255 . . . . . . 7  class  (  seq  0 ( ( e  e.  _V ,  g  e.  _V  |->  ( ( r splitFld1  e ) `  g
) ) ,  ( f  u.  { <. 0 ,  <. r ,  (  _I  |`  ( Base `  r ) )
>. >. } ) ) `
 ( # `  p
) )
3919, 38wceq 1623 . . . . . 6  wff  x  =  (  seq  0 ( ( e  e.  _V ,  g  e.  _V  |->  ( ( r splitFld1  e ) `
 g ) ) ,  ( f  u. 
{ <. 0 ,  <. r ,  (  _I  |`  ( Base `  r ) )
>. >. } ) ) `
 ( # `  p
) )
4017, 39wa 358 . . . . 5  wff  ( f 
Isom  <  ,  ( lt
`  r ) ( ( 1 ... ( # `
 p ) ) ,  p )  /\  x  =  (  seq  0 ( ( e  e.  _V ,  g  e.  _V  |->  ( ( r splitFld1  e ) `  g
) ) ,  ( f  u.  { <. 0 ,  <. r ,  (  _I  |`  ( Base `  r ) )
>. >. } ) ) `
 ( # `  p
) ) )
4140, 15wex 1528 . . . 4  wff  E. f
( f  Isom  <  ,  ( lt `  r
) ( ( 1 ... ( # `  p
) ) ,  p
)  /\  x  =  (  seq  0 ( ( e  e.  _V , 
g  e.  _V  |->  ( ( r splitFld1  e ) `  g
) ) ,  ( f  u.  { <. 0 ,  <. r ,  (  _I  |`  ( Base `  r ) )
>. >. } ) ) `
 ( # `  p
) ) )
4241, 18cio 5217 . . 3  class  ( iota
x E. f ( f  Isom  <  ,  ( lt `  r ) ( ( 1 ... ( # `  p
) ) ,  p
)  /\  x  =  (  seq  0 ( ( e  e.  _V , 
g  e.  _V  |->  ( ( r splitFld1  e ) `  g
) ) ,  ( f  u.  { <. 0 ,  <. r ,  (  _I  |`  ( Base `  r ) )
>. >. } ) ) `
 ( # `  p
) ) ) )
432, 3, 4, 4, 42cmpt2 5860 . 2  class  ( r  e.  _V ,  p  e.  _V  |->  ( iota x E. f ( f  Isom  <  ,  ( lt `  r ) ( ( 1 ... ( # `  p ) ) ,  p )  /\  x  =  (  seq  0
( ( e  e. 
_V ,  g  e. 
_V  |->  ( ( r splitFld1  e ) `  g ) ) ,  ( f  u.  { <. 0 ,  <. r ,  (  _I  |`  ( Base `  r ) ) >. >. } ) ) `  ( # `  p ) ) ) ) )
441, 43wceq 1623 1  wff splitFld  =  ( r  e.  _V ,  p  e.  _V  |->  ( iota
x E. f ( f  Isom  <  ,  ( lt `  r ) ( ( 1 ... ( # `  p
) ) ,  p
)  /\  x  =  (  seq  0 ( ( e  e.  _V , 
g  e.  _V  |->  ( ( r splitFld1  e ) `  g
) ) ,  ( f  u.  { <. 0 ,  <. r ,  (  _I  |`  ( Base `  r ) )
>. >. } ) ) `
 ( # `  p
) ) ) ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator