Definition df-sfl1 31535

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

Step	Hyp	Ref	Expression
1		csf1 31527	. 2 class splitFld1
2		vr	. . 3 setvar r
3		vj	. . 3 setvar j
4		cvv 3200	. . 3 class _V
5		vp	. . . 4 setvar p
6	2	cv 1482	. . . . 5 class r
7		cpl1 19547	. . . . 5 class Poly1
8	6, 7	cfv 5888	. . . 4 class (Poly1 ` r )
9		c1 9937	. . . . . . 7 class 1
10	5	cv 1482	. . . . . . . 8 class p
11		cdg1 23814	. . . . . . . 8 class deg1
12	6, 10, 11	co 6650	. . . . . . 7 class ( r deg1 p )
13		cfz 12326	. . . . . . 7 class ...
14	9, 12, 13	co 6650	. . . . . 6 class ( 1 ... ( r deg1 p ) )
15		ccrd 8761	. . . . . 6 class card
16	14, 15	cfv 5888	. . . . 5 class ( card ` ( 1 ... ( r deg1 p ) ) )
17		vs	. . . . . . 7 setvar s
18		vf	. . . . . . 7 setvar f
19		vm	. . . . . . . 8 setvar m
20	17	cv 1482	. . . . . . . . 9 class s
21		cmpl 19353	. . . . . . . . 9 class mPoly
22	20, 21	cfv 5888	. . . . . . . 8 class ( mPoly ` s )
23		vb	. . . . . . . . 9 setvar b
24		vg	. . . . . . . . . . . . 13 setvar g
25	24	cv 1482	. . . . . . . . . . . 12 class g
26	18	cv 1482	. . . . . . . . . . . . 13 class f
27	10, 26	ccom 5118	. . . . . . . . . . . 12 class ( p o. f )
28	19	cv 1482	. . . . . . . . . . . . 13 class m
29		cdsr 18638	. . . . . . . . . . . . 13 class ||r
30	28, 29	cfv 5888	. . . . . . . . . . . 12 class ( ||r ` m )
31	25, 27, 30	wbr 4653	. . . . . . . . . . 11 wff g ( ||r ` m ) ( p o. f )
32	20, 25, 11	co 6650	. . . . . . . . . . . 12 class ( s deg1 g )
33		clt 10074	. . . . . . . . . . . 12 class <
34	9, 32, 33	wbr 4653	. . . . . . . . . . 11 wff 1 < ( s deg1 g )
35	31, 34	wa 384	. . . . . . . . . 10 wff ( g ( ||r ` m ) ( p o. f ) /\ 1 < ( s deg1 g ) )
36		cmn1 23885	. . . . . . . . . . . 12 class Monic1p
37	20, 36	cfv 5888	. . . . . . . . . . 11 class (Monic1p ` s )
38		cir 18640	. . . . . . . . . . . 12 class Irred
39	28, 38	cfv 5888	. . . . . . . . . . 11 class (Irred ` m )
40	37, 39	cin 3573	. . . . . . . . . 10 class ( (Monic1p ` s ) i^i (Irred ` m ) )
41	35, 24, 40	crab 2916	. . . . . . . . 9 class { g e. ( (Monic1p ` s ) i^i (Irred ` m ) ) | ( g ( ||r ` m ) ( p o. f ) /\ 1 < ( s deg1 g ) ) }
42		c0g 16100	. . . . . . . . . . . . 13 class 0g
43	28, 42	cfv 5888	. . . . . . . . . . . 12 class ( 0g ` m )
44	27, 43	wceq 1483	. . . . . . . . . . 11 wff ( p o. f ) = ( 0g ` m )
45	23	cv 1482	. . . . . . . . . . . 12 class b
46		c0 3915	. . . . . . . . . . . 12 class (/)
47	45, 46	wceq 1483	. . . . . . . . . . 11 wff b = (/)
48	44, 47	wo 383	. . . . . . . . . 10 wff ( ( p o. f ) = ( 0g ` m ) \/ b = (/) )
49	20, 26	cop 4183	. . . . . . . . . 10 class <. s , f >.
50		vh	. . . . . . . . . . 11 setvar h
51		cglb 16943	. . . . . . . . . . . 12 class glb
52	45, 51	cfv 5888	. . . . . . . . . . 11 class ( glb ` b )
53		vt	. . . . . . . . . . . 12 setvar t
54	50	cv 1482	. . . . . . . . . . . . 13 class h
55		cpfl 31526	. . . . . . . . . . . . 13 class polyFld
56	20, 54, 55	co 6650	. . . . . . . . . . . 12 class ( s polyFld h )
57	53	cv 1482	. . . . . . . . . . . . . 14 class t
58		c1st 7166	. . . . . . . . . . . . . 14 class 1st
59	57, 58	cfv 5888	. . . . . . . . . . . . 13 class ( 1st ` t )
60		c2nd 7167	. . . . . . . . . . . . . . 15 class 2nd
61	57, 60	cfv 5888	. . . . . . . . . . . . . 14 class ( 2nd ` t )
62	26, 61	ccom 5118	. . . . . . . . . . . . 13 class ( f o. ( 2nd ` t ) )
63	59, 62	cop 4183	. . . . . . . . . . . 12 class <. ( 1st ` t ) , ( f o. ( 2nd ` t ) ) >.
64	53, 56, 63	csb 3533	. . . . . . . . . . 11 class [_ ( s polyFld h ) / t ]_ <. ( 1st ` t ) , ( f o. ( 2nd ` t ) ) >.
65	50, 52, 64	csb 3533	. . . . . . . . . 10 class [_ ( glb ` b ) / h ]_ [_ ( s polyFld h ) / t ]_ <. ( 1st ` t ) , ( f o. ( 2nd ` t ) ) >.
66	48, 49, 65	cif 4086	. . . . . . . . 9 class if ( ( ( p o. f ) = ( 0g ` m ) \/ b = (/) ) , <. s , f >. , [_ ( glb ` b ) / h ]_ [_ ( s polyFld h ) / t ]_ <. ( 1st ` t ) , ( f o. ( 2nd ` t ) ) >. )
67	23, 41, 66	csb 3533	. . . . . . . 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 ) ) >. )
68	19, 22, 67	csb 3533	. . . . . . 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 ) ) >. )
69	17, 18, 4, 4, 68	cmpt2 6652	. . . . . 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 ) ) >. ) )
70	3	cv 1482	. . . . . 6 class j
71	69, 70	crdg 7505	. . . . 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 )
72	16, 71	cfv 5888	. . . 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 ) ) ) )
73	5, 8, 72	cmpt 4729	. . 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 ) ) ) ) )
74	2, 3, 4, 4, 73	cmpt2 6652	. 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 ) ) ) ) ) )
75	1, 74	wceq 1483	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 ) ) ) ) ) )

This definition is referenced by: (None)