Definition df-sfl 31536

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

Step	Hyp	Ref	Expression
1		csf 31528	. 2 class splitFld
2		vr	. . 3 setvar r
3		vp	. . 3 setvar p
4		cvv 3200	. . 3 class _V
5		c1 9937	. . . . . . . 8 class 1
6	3	cv 1482	. . . . . . . . 9 class p
7		chash 13117	. . . . . . . . 9 class #
8	6, 7	cfv 5888	. . . . . . . 8 class ( # ` p )
9		cfz 12326	. . . . . . . 8 class ...
10	5, 8, 9	co 6650	. . . . . . 7 class ( 1 ... ( # ` p ) )
11		clt 10074	. . . . . . 7 class <
12	2	cv 1482	. . . . . . . 8 class r
13		cplt 16941	. . . . . . . 8 class lt
14	12, 13	cfv 5888	. . . . . . 7 class ( lt ` r )
15		vf	. . . . . . . 8 setvar f
16	15	cv 1482	. . . . . . 7 class f
17	10, 6, 11, 14, 16	wiso 5889	. . . . . 6 wff f Isom < , ( lt ` r ) ( ( 1 ... ( # ` p ) ) , p )
18		vx	. . . . . . . 8 setvar x
19	18	cv 1482	. . . . . . 7 class x
20		ve	. . . . . . . . . 10 setvar e
21		vg	. . . . . . . . . 10 setvar g
22	21	cv 1482	. . . . . . . . . . 11 class g
23	20	cv 1482	. . . . . . . . . . . 12 class e
24		csf1 31527	. . . . . . . . . . . 12 class splitFld1
25	12, 23, 24	co 6650	. . . . . . . . . . 11 class ( r splitFld1 e )
26	22, 25	cfv 5888	. . . . . . . . . 10 class ( ( r splitFld1 e ) ` g )
27	20, 21, 4, 4, 26	cmpt2 6652	. . . . . . . . 9 class ( e e. _V , g e. _V |-> ( ( r splitFld1 e ) ` g ) )
28		cc0 9936	. . . . . . . . . . . 12 class 0
29		cid 5023	. . . . . . . . . . . . . 14 class _I
30		cbs 15857	. . . . . . . . . . . . . . 15 class Base
31	12, 30	cfv 5888	. . . . . . . . . . . . . 14 class ( Base ` r )
32	29, 31	cres 5116	. . . . . . . . . . . . 13 class ( _I |` ( Base ` r ) )
33	12, 32	cop 4183	. . . . . . . . . . . 12 class <. r , ( _I |` ( Base ` r ) ) >.
34	28, 33	cop 4183	. . . . . . . . . . 11 class <. 0 , <. r , ( _I |` ( Base ` r ) ) >. >.
35	34	csn 4177	. . . . . . . . . 10 class { <. 0 , <. r , ( _I |` ( Base ` r ) ) >. >. }
36	16, 35	cun 3572	. . . . . . . . 9 class ( f u. { <. 0 , <. r , ( _I |` ( Base ` r ) ) >. >. } )
37	27, 36, 28	cseq 12801	. . . . . . . 8 class seq 0 ( ( e e. _V , g e. _V |-> ( ( r splitFld1 e ) ` g ) ) , ( f u. { <. 0 , <. r , ( _I |` ( Base ` r ) ) >. >. } ) )
38	8, 37	cfv 5888	. . . . . . 7 class ( seq 0 ( ( e e. _V , g e. _V |-> ( ( r splitFld1 e ) ` g ) ) , ( f u. { <. 0 , <. r , ( _I |` ( Base ` r ) ) >. >. } ) ) ` ( # ` p ) )
39	19, 38	wceq 1483	. . . . . 6 wff x = ( seq 0 ( ( e e. _V , g e. _V |-> ( ( r splitFld1 e ) ` g ) ) , ( f u. { <. 0 , <. r , ( _I |` ( Base ` r ) ) >. >. } ) ) ` ( # ` p ) )
40	17, 39	wa 384	. . . . 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 ) ) )
41	40, 15	wex 1704	. . . 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 ) ) )
42	41, 18	cio 5849	. . 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 ) ) ) )
43	2, 3, 4, 4, 42	cmpt2 6652	. 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 ) ) ) ) )
44	1, 43	wceq 1483	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 ) ) ) ) )

This definition is referenced by: (None)