Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sfl1 Structured version   Visualization version   GIF version

Definition df-sfl1 33338
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 = (𝑟 ∈ V, 𝑗 ∈ V ↦ (𝑝 ∈ (Poly1𝑟) ↦ (rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ( mPoly ‘𝑠) / 𝑚{𝑔 ∈ ((Monic1p𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r𝑚)(𝑝𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏if(((𝑝𝑓) = (0g𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, (glb‘𝑏) / (𝑠 polyFld ) / 𝑡⟨(1st𝑡), (𝑓 ∘ (2nd𝑡))⟩)), 𝑗)‘(card‘(1...(𝑟 deg1 𝑝))))))
Distinct variable group:   𝑓,𝑏,𝑔,,𝑗,𝑚,𝑝,𝑟,𝑠,𝑡

Detailed syntax breakdown of Definition df-sfl1
StepHypRef Expression
1 csf1 33330 . 2 class splitFld1
2 vr . . 3 setvar 𝑟
3 vj . . 3 setvar 𝑗
4 cvv 3420 . . 3 class V
5 vp . . . 4 setvar 𝑝
62cv 1542 . . . . 5 class 𝑟
7 cpl1 21122 . . . . 5 class Poly1
86, 7cfv 6397 . . . 4 class (Poly1𝑟)
9 c1 10754 . . . . . . 7 class 1
105cv 1542 . . . . . . . 8 class 𝑝
11 cdg1 24973 . . . . . . . 8 class deg1
126, 10, 11co 7231 . . . . . . 7 class (𝑟 deg1 𝑝)
13 cfz 13119 . . . . . . 7 class ...
149, 12, 13co 7231 . . . . . 6 class (1...(𝑟 deg1 𝑝))
15 ccrd 9575 . . . . . 6 class card
1614, 15cfv 6397 . . . . 5 class (card‘(1...(𝑟 deg1 𝑝)))
17 vs . . . . . . 7 setvar 𝑠
18 vf . . . . . . 7 setvar 𝑓
19 vm . . . . . . . 8 setvar 𝑚
2017cv 1542 . . . . . . . . 9 class 𝑠
21 cmpl 20889 . . . . . . . . 9 class mPoly
2220, 21cfv 6397 . . . . . . . 8 class ( mPoly ‘𝑠)
23 vb . . . . . . . . 9 setvar 𝑏
24 vg . . . . . . . . . . . . 13 setvar 𝑔
2524cv 1542 . . . . . . . . . . . 12 class 𝑔
2618cv 1542 . . . . . . . . . . . . 13 class 𝑓
2710, 26ccom 5569 . . . . . . . . . . . 12 class (𝑝𝑓)
2819cv 1542 . . . . . . . . . . . . 13 class 𝑚
29 cdsr 19680 . . . . . . . . . . . . 13 class r
3028, 29cfv 6397 . . . . . . . . . . . 12 class (∥r𝑚)
3125, 27, 30wbr 5067 . . . . . . . . . . 11 wff 𝑔(∥r𝑚)(𝑝𝑓)
3220, 25, 11co 7231 . . . . . . . . . . . 12 class (𝑠 deg1 𝑔)
33 clt 10891 . . . . . . . . . . . 12 class <
349, 32, 33wbr 5067 . . . . . . . . . . 11 wff 1 < (𝑠 deg1 𝑔)
3531, 34wa 399 . . . . . . . . . 10 wff (𝑔(∥r𝑚)(𝑝𝑓) ∧ 1 < (𝑠 deg1 𝑔))
36 cmn1 25047 . . . . . . . . . . . 12 class Monic1p
3720, 36cfv 6397 . . . . . . . . . . 11 class (Monic1p𝑠)
38 cir 19682 . . . . . . . . . . . 12 class Irred
3928, 38cfv 6397 . . . . . . . . . . 11 class (Irred‘𝑚)
4037, 39cin 3879 . . . . . . . . . 10 class ((Monic1p𝑠) ∩ (Irred‘𝑚))
4135, 24, 40crab 3066 . . . . . . . . 9 class {𝑔 ∈ ((Monic1p𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r𝑚)(𝑝𝑓) ∧ 1 < (𝑠 deg1 𝑔))}
42 c0g 16968 . . . . . . . . . . . . 13 class 0g
4328, 42cfv 6397 . . . . . . . . . . . 12 class (0g𝑚)
4427, 43wceq 1543 . . . . . . . . . . 11 wff (𝑝𝑓) = (0g𝑚)
4523cv 1542 . . . . . . . . . . . 12 class 𝑏
46 c0 4251 . . . . . . . . . . . 12 class
4745, 46wceq 1543 . . . . . . . . . . 11 wff 𝑏 = ∅
4844, 47wo 847 . . . . . . . . . 10 wff ((𝑝𝑓) = (0g𝑚) ∨ 𝑏 = ∅)
4920, 26cop 4561 . . . . . . . . . 10 class 𝑠, 𝑓
50 vh . . . . . . . . . . 11 setvar
51 cglb 17841 . . . . . . . . . . . 12 class glb
5245, 51cfv 6397 . . . . . . . . . . 11 class (glb‘𝑏)
53 vt . . . . . . . . . . . 12 setvar 𝑡
5450cv 1542 . . . . . . . . . . . . 13 class
55 cpfl 33329 . . . . . . . . . . . . 13 class polyFld
5620, 54, 55co 7231 . . . . . . . . . . . 12 class (𝑠 polyFld )
5753cv 1542 . . . . . . . . . . . . . 14 class 𝑡
58 c1st 7777 . . . . . . . . . . . . . 14 class 1st
5957, 58cfv 6397 . . . . . . . . . . . . 13 class (1st𝑡)
60 c2nd 7778 . . . . . . . . . . . . . . 15 class 2nd
6157, 60cfv 6397 . . . . . . . . . . . . . 14 class (2nd𝑡)
6226, 61ccom 5569 . . . . . . . . . . . . 13 class (𝑓 ∘ (2nd𝑡))
6359, 62cop 4561 . . . . . . . . . . . 12 class ⟨(1st𝑡), (𝑓 ∘ (2nd𝑡))⟩
6453, 56, 63csb 3825 . . . . . . . . . . 11 class (𝑠 polyFld ) / 𝑡⟨(1st𝑡), (𝑓 ∘ (2nd𝑡))⟩
6550, 52, 64csb 3825 . . . . . . . . . 10 class (glb‘𝑏) / (𝑠 polyFld ) / 𝑡⟨(1st𝑡), (𝑓 ∘ (2nd𝑡))⟩
6648, 49, 65cif 4453 . . . . . . . . 9 class if(((𝑝𝑓) = (0g𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, (glb‘𝑏) / (𝑠 polyFld ) / 𝑡⟨(1st𝑡), (𝑓 ∘ (2nd𝑡))⟩)
6723, 41, 66csb 3825 . . . . . . . 8 class {𝑔 ∈ ((Monic1p𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r𝑚)(𝑝𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏if(((𝑝𝑓) = (0g𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, (glb‘𝑏) / (𝑠 polyFld ) / 𝑡⟨(1st𝑡), (𝑓 ∘ (2nd𝑡))⟩)
6819, 22, 67csb 3825 . . . . . . 7 class ( mPoly ‘𝑠) / 𝑚{𝑔 ∈ ((Monic1p𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r𝑚)(𝑝𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏if(((𝑝𝑓) = (0g𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, (glb‘𝑏) / (𝑠 polyFld ) / 𝑡⟨(1st𝑡), (𝑓 ∘ (2nd𝑡))⟩)
6917, 18, 4, 4, 68cmpo 7233 . . . . . 6 class (𝑠 ∈ V, 𝑓 ∈ V ↦ ( mPoly ‘𝑠) / 𝑚{𝑔 ∈ ((Monic1p𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r𝑚)(𝑝𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏if(((𝑝𝑓) = (0g𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, (glb‘𝑏) / (𝑠 polyFld ) / 𝑡⟨(1st𝑡), (𝑓 ∘ (2nd𝑡))⟩))
703cv 1542 . . . . . 6 class 𝑗
7169, 70crdg 8165 . . . . 5 class rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ( mPoly ‘𝑠) / 𝑚{𝑔 ∈ ((Monic1p𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r𝑚)(𝑝𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏if(((𝑝𝑓) = (0g𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, (glb‘𝑏) / (𝑠 polyFld ) / 𝑡⟨(1st𝑡), (𝑓 ∘ (2nd𝑡))⟩)), 𝑗)
7216, 71cfv 6397 . . . 4 class (rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ( mPoly ‘𝑠) / 𝑚{𝑔 ∈ ((Monic1p𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r𝑚)(𝑝𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏if(((𝑝𝑓) = (0g𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, (glb‘𝑏) / (𝑠 polyFld ) / 𝑡⟨(1st𝑡), (𝑓 ∘ (2nd𝑡))⟩)), 𝑗)‘(card‘(1...(𝑟 deg1 𝑝))))
735, 8, 72cmpt 5149 . . 3 class (𝑝 ∈ (Poly1𝑟) ↦ (rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ( mPoly ‘𝑠) / 𝑚{𝑔 ∈ ((Monic1p𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r𝑚)(𝑝𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏if(((𝑝𝑓) = (0g𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, (glb‘𝑏) / (𝑠 polyFld ) / 𝑡⟨(1st𝑡), (𝑓 ∘ (2nd𝑡))⟩)), 𝑗)‘(card‘(1...(𝑟 deg1 𝑝)))))
742, 3, 4, 4, 73cmpo 7233 . 2 class (𝑟 ∈ V, 𝑗 ∈ V ↦ (𝑝 ∈ (Poly1𝑟) ↦ (rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ( mPoly ‘𝑠) / 𝑚{𝑔 ∈ ((Monic1p𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r𝑚)(𝑝𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏if(((𝑝𝑓) = (0g𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, (glb‘𝑏) / (𝑠 polyFld ) / 𝑡⟨(1st𝑡), (𝑓 ∘ (2nd𝑡))⟩)), 𝑗)‘(card‘(1...(𝑟 deg1 𝑝))))))
751, 74wceq 1543 1 wff splitFld1 = (𝑟 ∈ V, 𝑗 ∈ V ↦ (𝑝 ∈ (Poly1𝑟) ↦ (rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ( mPoly ‘𝑠) / 𝑚{𝑔 ∈ ((Monic1p𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r𝑚)(𝑝𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏if(((𝑝𝑓) = (0g𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, (glb‘𝑏) / (𝑠 polyFld ) / 𝑡⟨(1st𝑡), (𝑓 ∘ (2nd𝑡))⟩)), 𝑗)‘(card‘(1...(𝑟 deg1 𝑝))))))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator