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 and a polynomial that we want to split, along with a tuple in the same format as the output. The output is a tuple where is the splitting field and is an injective homomorphism from the original field . 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 Poly1 mPoly Monic1p Irred r deg1 polyFld deg1
Distinct variable group:   ,,,,,,,,,

Detailed syntax breakdown of Definition df-sfl1
StepHypRef Expression
1 csf1 25067 . 2 splitFld1
2 vr . . 3
3 vj . . 3
4 cvv 2956 . . 3
5 vp . . . 4
62cv 1651 . . . . 5
7 cpl1 16571 . . . . 5 Poly1
86, 7cfv 5454 . . . 4 Poly1
9 c1 8991 . . . . . . 7
105cv 1651 . . . . . . . 8
11 cdg1 19977 . . . . . . . 8 deg1
126, 10, 11co 6081 . . . . . . 7 deg1
13 cfz 11043 . . . . . . 7
149, 12, 13co 6081 . . . . . 6 deg1
15 ccrd 7822 . . . . . 6
1614, 15cfv 5454 . . . . 5 deg1
17 vs . . . . . . 7
18 vf . . . . . . 7
19 vm . . . . . . . 8
2017cv 1651 . . . . . . . . 9
21 cmpl 16408 . . . . . . . . 9 mPoly
2220, 21cfv 5454 . . . . . . . 8 mPoly
23 vb . . . . . . . . 9
24 vg . . . . . . . . . . . . 13
2524cv 1651 . . . . . . . . . . . 12
2618cv 1651 . . . . . . . . . . . . 13
2710, 26ccom 4882 . . . . . . . . . . . 12
2819cv 1651 . . . . . . . . . . . . 13
29 cdsr 15743 . . . . . . . . . . . . 13 r
3028, 29cfv 5454 . . . . . . . . . . . 12 r
3125, 27, 30wbr 4212 . . . . . . . . . . 11 r
3220, 25, 11co 6081 . . . . . . . . . . . 12 deg1
33 clt 9120 . . . . . . . . . . . 12
349, 32, 33wbr 4212 . . . . . . . . . . 11 deg1
3531, 34wa 359 . . . . . . . . . 10 r deg1
36 cmn1 20048 . . . . . . . . . . . 12 Monic1p
3720, 36cfv 5454 . . . . . . . . . . 11 Monic1p
38 cir 15745 . . . . . . . . . . . 12 Irred
3928, 38cfv 5454 . . . . . . . . . . 11 Irred
4037, 39cin 3319 . . . . . . . . . 10 Monic1p Irred
4135, 24, 40crab 2709 . . . . . . . . 9 Monic1p Irred r deg1
42 c0g 13723 . . . . . . . . . . . . 13
4328, 42cfv 5454 . . . . . . . . . . . 12
4427, 43wceq 1652 . . . . . . . . . . 11
4523cv 1651 . . . . . . . . . . . 12
46 c0 3628 . . . . . . . . . . . 12
4745, 46wceq 1652 . . . . . . . . . . 11
4844, 47wo 358 . . . . . . . . . 10
4920, 26cop 3817 . . . . . . . . . 10
50 vh . . . . . . . . . . 11
51 cglb 14400 . . . . . . . . . . . 12
5245, 51cfv 5454 . . . . . . . . . . 11
53 vt . . . . . . . . . . . 12
5450cv 1651 . . . . . . . . . . . . 13
55 cpfl 25066 . . . . . . . . . . . . 13 polyFld
5620, 54, 55co 6081 . . . . . . . . . . . 12 polyFld
5753cv 1651 . . . . . . . . . . . . . 14
58 c1st 6347 . . . . . . . . . . . . . 14
5957, 58cfv 5454 . . . . . . . . . . . . 13
60 c2nd 6348 . . . . . . . . . . . . . . 15
6157, 60cfv 5454 . . . . . . . . . . . . . 14
6226, 61ccom 4882 . . . . . . . . . . . . 13
6359, 62cop 3817 . . . . . . . . . . . 12
6453, 56, 63csb 3251 . . . . . . . . . . 11 polyFld
6550, 52, 64csb 3251 . . . . . . . . . 10 polyFld
6648, 49, 65cif 3739 . . . . . . . . 9 polyFld
6723, 41, 66csb 3251 . . . . . . . 8 Monic1p Irred r deg1 polyFld
6819, 22, 67csb 3251 . . . . . . 7 mPoly Monic1p Irred r deg1 polyFld
6917, 18, 4, 4, 68cmpt2 6083 . . . . . 6 mPoly Monic1p Irred r deg1 polyFld
703cv 1651 . . . . . 6
7169, 70crdg 6667 . . . . 5 mPoly Monic1p Irred r deg1 polyFld
7216, 71cfv 5454 . . . 4 mPoly Monic1p Irred r deg1 polyFld deg1
735, 8, 72cmpt 4266 . . 3 Poly1 mPoly Monic1p Irred r deg1 polyFld deg1
742, 3, 4, 4, 73cmpt2 6083 . 2 Poly1 mPoly Monic1p Irred r deg1 polyFld deg1
751, 74wceq 1652 1 splitFld1 Poly1 mPoly Monic1p Irred r deg1 polyFld deg1
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator