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 35612
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 ↦ (Poly1𝑠) / 𝑚{𝑔 ∈ ((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 35599 . 2 class splitFld1
2 vr . . 3 setvar 𝑟
3 vj . . 3 setvar 𝑗
4 cvv 3488 . . 3 class V
5 vp . . . 4 setvar 𝑝
62cv 1536 . . . . 5 class 𝑟
7 cpl1 22199 . . . . 5 class Poly1
86, 7cfv 6573 . . . 4 class (Poly1𝑟)
9 c1 11185 . . . . . . 7 class 1
105cv 1536 . . . . . . . 8 class 𝑝
11 cdg1 26113 . . . . . . . 8 class deg1
126, 10, 11co 7448 . . . . . . 7 class (𝑟deg1𝑝)
13 cfz 13567 . . . . . . 7 class ...
149, 12, 13co 7448 . . . . . 6 class (1...(𝑟deg1𝑝))
15 ccrd 10004 . . . . . 6 class card
1614, 15cfv 6573 . . . . 5 class (card‘(1...(𝑟deg1𝑝)))
17 vs . . . . . . 7 setvar 𝑠
18 vf . . . . . . 7 setvar 𝑓
19 vm . . . . . . . 8 setvar 𝑚
2017cv 1536 . . . . . . . . 9 class 𝑠
2120, 7cfv 6573 . . . . . . . 8 class (Poly1𝑠)
22 vb . . . . . . . . 9 setvar 𝑏
23 vg . . . . . . . . . . . . 13 setvar 𝑔
2423cv 1536 . . . . . . . . . . . 12 class 𝑔
2518cv 1536 . . . . . . . . . . . . 13 class 𝑓
2610, 25ccom 5704 . . . . . . . . . . . 12 class (𝑝𝑓)
2719cv 1536 . . . . . . . . . . . . 13 class 𝑚
28 cdsr 20380 . . . . . . . . . . . . 13 class r
2927, 28cfv 6573 . . . . . . . . . . . 12 class (∥r𝑚)
3024, 26, 29wbr 5166 . . . . . . . . . . 11 wff 𝑔(∥r𝑚)(𝑝𝑓)
3120, 24, 11co 7448 . . . . . . . . . . . 12 class (𝑠deg1𝑔)
32 clt 11324 . . . . . . . . . . . 12 class <
339, 31, 32wbr 5166 . . . . . . . . . . 11 wff 1 < (𝑠deg1𝑔)
3430, 33wa 395 . . . . . . . . . 10 wff (𝑔(∥r𝑚)(𝑝𝑓) ∧ 1 < (𝑠deg1𝑔))
35 cmn1 26185 . . . . . . . . . . . 12 class Monic1p
3620, 35cfv 6573 . . . . . . . . . . 11 class (Monic1p𝑠)
37 cir 20382 . . . . . . . . . . . 12 class Irred
3827, 37cfv 6573 . . . . . . . . . . 11 class (Irred‘𝑚)
3936, 38cin 3975 . . . . . . . . . 10 class ((Monic1p𝑠) ∩ (Irred‘𝑚))
4034, 23, 39crab 3443 . . . . . . . . 9 class {𝑔 ∈ ((Monic1p𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r𝑚)(𝑝𝑓) ∧ 1 < (𝑠deg1𝑔))}
41 c0g 17499 . . . . . . . . . . . . 13 class 0g
4227, 41cfv 6573 . . . . . . . . . . . 12 class (0g𝑚)
4326, 42wceq 1537 . . . . . . . . . . 11 wff (𝑝𝑓) = (0g𝑚)
4422cv 1536 . . . . . . . . . . . 12 class 𝑏
45 c0 4352 . . . . . . . . . . . 12 class
4644, 45wceq 1537 . . . . . . . . . . 11 wff 𝑏 = ∅
4743, 46wo 846 . . . . . . . . . 10 wff ((𝑝𝑓) = (0g𝑚) ∨ 𝑏 = ∅)
4820, 25cop 4654 . . . . . . . . . 10 class 𝑠, 𝑓
49 vh . . . . . . . . . . 11 setvar
50 cglb 18380 . . . . . . . . . . . 12 class glb
5144, 50cfv 6573 . . . . . . . . . . 11 class (glb‘𝑏)
52 vt . . . . . . . . . . . 12 setvar 𝑡
5349cv 1536 . . . . . . . . . . . . 13 class
54 cpfl 35598 . . . . . . . . . . . . 13 class polyFld
5520, 53, 54co 7448 . . . . . . . . . . . 12 class (𝑠 polyFld )
5652cv 1536 . . . . . . . . . . . . . 14 class 𝑡
57 c1st 8028 . . . . . . . . . . . . . 14 class 1st
5856, 57cfv 6573 . . . . . . . . . . . . 13 class (1st𝑡)
59 c2nd 8029 . . . . . . . . . . . . . . 15 class 2nd
6056, 59cfv 6573 . . . . . . . . . . . . . 14 class (2nd𝑡)
6125, 60ccom 5704 . . . . . . . . . . . . 13 class (𝑓 ∘ (2nd𝑡))
6258, 61cop 4654 . . . . . . . . . . . 12 class ⟨(1st𝑡), (𝑓 ∘ (2nd𝑡))⟩
6352, 55, 62csb 3921 . . . . . . . . . . 11 class (𝑠 polyFld ) / 𝑡⟨(1st𝑡), (𝑓 ∘ (2nd𝑡))⟩
6449, 51, 63csb 3921 . . . . . . . . . 10 class (glb‘𝑏) / (𝑠 polyFld ) / 𝑡⟨(1st𝑡), (𝑓 ∘ (2nd𝑡))⟩
6547, 48, 64cif 4548 . . . . . . . . 9 class if(((𝑝𝑓) = (0g𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, (glb‘𝑏) / (𝑠 polyFld ) / 𝑡⟨(1st𝑡), (𝑓 ∘ (2nd𝑡))⟩)
6622, 40, 65csb 3921 . . . . . . . 8 class {𝑔 ∈ ((Monic1p𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r𝑚)(𝑝𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏if(((𝑝𝑓) = (0g𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, (glb‘𝑏) / (𝑠 polyFld ) / 𝑡⟨(1st𝑡), (𝑓 ∘ (2nd𝑡))⟩)
6719, 21, 66csb 3921 . . . . . . 7 class (Poly1𝑠) / 𝑚{𝑔 ∈ ((Monic1p𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r𝑚)(𝑝𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏if(((𝑝𝑓) = (0g𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, (glb‘𝑏) / (𝑠 polyFld ) / 𝑡⟨(1st𝑡), (𝑓 ∘ (2nd𝑡))⟩)
6817, 18, 4, 4, 67cmpo 7450 . . . . . 6 class (𝑠 ∈ V, 𝑓 ∈ V ↦ (Poly1𝑠) / 𝑚{𝑔 ∈ ((Monic1p𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r𝑚)(𝑝𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏if(((𝑝𝑓) = (0g𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, (glb‘𝑏) / (𝑠 polyFld ) / 𝑡⟨(1st𝑡), (𝑓 ∘ (2nd𝑡))⟩))
693cv 1536 . . . . . 6 class 𝑗
7068, 69crdg 8465 . . . . 5 class rec((𝑠 ∈ V, 𝑓 ∈ V ↦ (Poly1𝑠) / 𝑚{𝑔 ∈ ((Monic1p𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r𝑚)(𝑝𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏if(((𝑝𝑓) = (0g𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, (glb‘𝑏) / (𝑠 polyFld ) / 𝑡⟨(1st𝑡), (𝑓 ∘ (2nd𝑡))⟩)), 𝑗)
7116, 70cfv 6573 . . . 4 class (rec((𝑠 ∈ V, 𝑓 ∈ V ↦ (Poly1𝑠) / 𝑚{𝑔 ∈ ((Monic1p𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r𝑚)(𝑝𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏if(((𝑝𝑓) = (0g𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, (glb‘𝑏) / (𝑠 polyFld ) / 𝑡⟨(1st𝑡), (𝑓 ∘ (2nd𝑡))⟩)), 𝑗)‘(card‘(1...(𝑟deg1𝑝))))
725, 8, 71cmpt 5249 . . 3 class (𝑝 ∈ (Poly1𝑟) ↦ (rec((𝑠 ∈ V, 𝑓 ∈ V ↦ (Poly1𝑠) / 𝑚{𝑔 ∈ ((Monic1p𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r𝑚)(𝑝𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏if(((𝑝𝑓) = (0g𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, (glb‘𝑏) / (𝑠 polyFld ) / 𝑡⟨(1st𝑡), (𝑓 ∘ (2nd𝑡))⟩)), 𝑗)‘(card‘(1...(𝑟deg1𝑝)))))
732, 3, 4, 4, 72cmpo 7450 . 2 class (𝑟 ∈ V, 𝑗 ∈ V ↦ (𝑝 ∈ (Poly1𝑟) ↦ (rec((𝑠 ∈ V, 𝑓 ∈ V ↦ (Poly1𝑠) / 𝑚{𝑔 ∈ ((Monic1p𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r𝑚)(𝑝𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏if(((𝑝𝑓) = (0g𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, (glb‘𝑏) / (𝑠 polyFld ) / 𝑡⟨(1st𝑡), (𝑓 ∘ (2nd𝑡))⟩)), 𝑗)‘(card‘(1...(𝑟deg1𝑝))))))
741, 73wceq 1537 1 wff splitFld1 = (𝑟 ∈ V, 𝑗 ∈ V ↦ (𝑝 ∈ (Poly1𝑟) ↦ (rec((𝑠 ∈ V, 𝑓 ∈ V ↦ (Poly1𝑠) / 𝑚{𝑔 ∈ ((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