Metamath Proof Explorer

Definition df-sfl

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)

Ref Expression
Assertion 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 ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csf 
 |-  splitFld
1 vr 
 |-  r
2 cvv 
 |-  _V
3 vp 
 |-  p
4 vx 
 |-  x
5 vf 
 |-  f
6 5 cv 
 |-  f
7 clt 
 |-  <
8 cplt 
 |-  lt
9 1 cv 
 |-  r
10 9 8 cfv 
 |-  ( lt ` r )
11 c1 
 |-  1
12 cfz 
 |-  ...
13 chash 
 |-  #
14 3 cv 
 |-  p
15 14 13 cfv 
 |-  ( # ` p )
16 11 15 12 co 
 |-  ( 1 ... ( # ` p ) )
17 16 14 7 10 6 wiso 
 |-  f Isom < , ( lt ` r ) ( ( 1 ... ( # ` p ) ) , p )
18 4 cv 
 |-  x
19 cc0 
 |-  0
20 ve 
 |-  e
21 vg 
 |-  g
22 csf1 
 |-  splitFld1
23 20 cv 
 |-  e
24 9 23 22 co 
 |-  ( r splitFld1 e )
25 21 cv 
 |-  g
26 25 24 cfv 
 |-  ( ( r splitFld1 e ) ` g )
27 20 21 2 2 26 cmpo 
 |-  ( e e. _V , g e. _V |-> ( ( r splitFld1 e ) ` g ) )
28 cid 
 |-  _I
29 cbs 
 |-  Base
30 9 29 cfv 
 |-  ( Base ` r )
31 28 30 cres 
 |-  ( _I |` ( Base ` r ) )
32 9 31 cop 
 |-  <. r , ( _I |` ( Base ` r ) ) >.
33 19 32 cop 
 |-  <. 0 , <. r , ( _I |` ( Base ` r ) ) >. >.
34 33 csn 
 |-  { <. 0 , <. r , ( _I |` ( Base ` r ) ) >. >. }
35 6 34 cun 
 |-  ( f u. { <. 0 , <. r , ( _I |` ( Base ` r ) ) >. >. } )
36 27 35 19 cseq 
 |-  seq 0 ( ( e e. _V , g e. _V |-> ( ( r splitFld1 e ) ` g ) ) , ( f u. { <. 0 , <. r , ( _I |` ( Base ` r ) ) >. >. } ) )
37 15 36 cfv 
 |-  ( seq 0 ( ( e e. _V , g e. _V |-> ( ( r splitFld1 e ) ` g ) ) , ( f u. { <. 0 , <. r , ( _I |` ( Base ` r ) ) >. >. } ) ) ` ( # ` p ) )
38 18 37 wceq 
 |-  x = ( seq 0 ( ( e e. _V , g e. _V |-> ( ( r splitFld1 e ) ` g ) ) , ( f u. { <. 0 , <. r , ( _I |` ( Base ` r ) ) >. >. } ) ) ` ( # ` p ) )
39 17 38 wa 
 |-  ( 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 ) ) )
40 39 5 wex 
 |-  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 ) ) )
41 40 4 cio 
 |-  ( 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 ) ) ) )
42 1 3 2 2 41 cmpo 
 |-  ( 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 ) ) ) ) )
43 0 42 wceq 
 |-  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 ) ) ) ) )