Definition df-sfl1 35629

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

Step	Hyp	Ref	Expression
1		csf1 35616	. 2 class splitFld1
2		vr	. . 3 setvar 𝑟
3		vj	. . 3 setvar 𝑗
4		cvv 3478	. . 3 class V
5		vp	. . . 4 setvar 𝑝
6	2	cv 1536	. . . . 5 class 𝑟
7		cpl1 22194	. . . . 5 class Poly1
8	6, 7	cfv 6563	. . . 4 class (Poly1‘𝑟)
9		c1 11154	. . . . . . 7 class 1
10	5	cv 1536	. . . . . . . 8 class 𝑝
11		cdg1 26108	. . . . . . . 8 class deg1
12	6, 10, 11	co 7431	. . . . . . 7 class (𝑟deg1𝑝)
13		cfz 13544	. . . . . . 7 class ...
14	9, 12, 13	co 7431	. . . . . 6 class (1...(𝑟deg1𝑝))
15		ccrd 9973	. . . . . 6 class card
16	14, 15	cfv 6563	. . . . 5 class (card‘(1...(𝑟deg1𝑝)))
17		vs	. . . . . . 7 setvar 𝑠
18		vf	. . . . . . 7 setvar 𝑓
19		vm	. . . . . . . 8 setvar 𝑚
20	17	cv 1536	. . . . . . . . 9 class 𝑠
21	20, 7	cfv 6563	. . . . . . . 8 class (Poly1‘𝑠)
22		vb	. . . . . . . . 9 setvar 𝑏
23		vg	. . . . . . . . . . . . 13 setvar 𝑔
24	23	cv 1536	. . . . . . . . . . . 12 class 𝑔
25	18	cv 1536	. . . . . . . . . . . . 13 class 𝑓
26	10, 25	ccom 5693	. . . . . . . . . . . 12 class (𝑝 ∘ 𝑓)
27	19	cv 1536	. . . . . . . . . . . . 13 class 𝑚
28		cdsr 20371	. . . . . . . . . . . . 13 class ∥r
29	27, 28	cfv 6563	. . . . . . . . . . . 12 class (∥r‘𝑚)
30	24, 26, 29	wbr 5148	. . . . . . . . . . 11 wff 𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓)
31	20, 24, 11	co 7431	. . . . . . . . . . . 12 class (𝑠deg1𝑔)
32		clt 11293	. . . . . . . . . . . 12 class <
33	9, 31, 32	wbr 5148	. . . . . . . . . . 11 wff 1 < (𝑠deg1𝑔)
34	30, 33	wa 395	. . . . . . . . . 10 wff (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))
35		cmn1 26180	. . . . . . . . . . . 12 class Monic1p
36	20, 35	cfv 6563	. . . . . . . . . . 11 class (Monic1p‘𝑠)
37		cir 20373	. . . . . . . . . . . 12 class Irred
38	27, 37	cfv 6563	. . . . . . . . . . 11 class (Irred‘𝑚)
39	36, 38	cin 3962	. . . . . . . . . 10 class ((Monic1p‘𝑠) ∩ (Irred‘𝑚))
40	34, 23, 39	crab 3433	. . . . . . . . 9 class {𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))}
41		c0g 17486	. . . . . . . . . . . . 13 class 0g
42	27, 41	cfv 6563	. . . . . . . . . . . 12 class (0g‘𝑚)
43	26, 42	wceq 1537	. . . . . . . . . . 11 wff (𝑝 ∘ 𝑓) = (0g‘𝑚)
44	22	cv 1536	. . . . . . . . . . . 12 class 𝑏
45		c0 4339	. . . . . . . . . . . 12 class ∅
46	44, 45	wceq 1537	. . . . . . . . . . 11 wff 𝑏 = ∅
47	43, 46	wo 847	. . . . . . . . . 10 wff ((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅)
48	20, 25	cop 4637	. . . . . . . . . 10 class ⟨𝑠, 𝑓⟩
49		vh	. . . . . . . . . . 11 setvar ℎ
50		cglb 18368	. . . . . . . . . . . 12 class glb
51	44, 50	cfv 6563	. . . . . . . . . . 11 class (glb‘𝑏)
52		vt	. . . . . . . . . . . 12 setvar 𝑡
53	49	cv 1536	. . . . . . . . . . . . 13 class ℎ
54		cpfl 35615	. . . . . . . . . . . . 13 class polyFld
55	20, 53, 54	co 7431	. . . . . . . . . . . 12 class (𝑠 polyFld ℎ)
56	52	cv 1536	. . . . . . . . . . . . . 14 class 𝑡
57		c1st 8011	. . . . . . . . . . . . . 14 class 1st
58	56, 57	cfv 6563	. . . . . . . . . . . . 13 class (1st ‘𝑡)
59		c2nd 8012	. . . . . . . . . . . . . . 15 class 2nd
60	56, 59	cfv 6563	. . . . . . . . . . . . . 14 class (2nd ‘𝑡)
61	25, 60	ccom 5693	. . . . . . . . . . . . 13 class (𝑓 ∘ (2nd ‘𝑡))
62	58, 61	cop 4637	. . . . . . . . . . . 12 class ⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
63	52, 55, 62	csb 3908	. . . . . . . . . . 11 class ⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
64	49, 51, 63	csb 3908	. . . . . . . . . 10 class ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
65	47, 48, 64	cif 4531	. . . . . . . . 9 class if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
66	22, 40, 65	csb 3908	. . . . . . . 8 class ⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
67	19, 21, 66	csb 3908	. . . . . . 7 class ⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
68	17, 18, 4, 4, 67	cmpo 7433	. . . . . 6 class (𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩))
69	3	cv 1536	. . . . . 6 class 𝑗
70	68, 69	crdg 8448	. . . . 5 class rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)), 𝑗)
71	16, 70	cfv 6563	. . . 4 class (rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)), 𝑗)‘(card‘(1...(𝑟deg1𝑝))))
72	5, 8, 71	cmpt 5231	. . 3 class (𝑝 ∈ (Poly1‘𝑟) ↦ (rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)), 𝑗)‘(card‘(1...(𝑟deg1𝑝)))))
73	2, 3, 4, 4, 72	cmpo 7433	. 2 class (𝑟 ∈ V, 𝑗 ∈ V ↦ (𝑝 ∈ (Poly1‘𝑟) ↦ (rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)), 𝑗)‘(card‘(1...(𝑟deg1𝑝))))))
74	1, 73	wceq 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𝑝))))))

This definition is referenced by: (None)