Definition df-sfl1 36007

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 35994	. 2 class splitFld1
2		vr	. . 3 setvar 𝑟
3		vj	. . 3 setvar 𝑗
4		cvv 3457	. . 3 class V
5		vp	. . . 4 setvar 𝑝
6	2	cv 1562	. . . . 5 class 𝑟
7		cpl1 22297	. . . . 5 class Poly1
8	6, 7	cfv 6525	. . . 4 class (Poly1‘𝑟)
9		c1 11089	. . . . . . 7 class 1
10	5	cv 1562	. . . . . . . 8 class 𝑝
11		cdg1 26172	. . . . . . . 8 class deg1
12	6, 10, 11	co 7400	. . . . . . 7 class (𝑟deg1𝑝)
13		cfz 13526	. . . . . . 7 class ...
14	9, 12, 13	co 7400	. . . . . 6 class (1...(𝑟deg1𝑝))
15		ccrd 9909	. . . . . 6 class card
16	14, 15	cfv 6525	. . . . 5 class (card‘(1...(𝑟deg1𝑝)))
17		vs	. . . . . . 7 setvar 𝑠
18		vf	. . . . . . 7 setvar 𝑓
19		vm	. . . . . . . 8 setvar 𝑚
20	17	cv 1562	. . . . . . . . 9 class 𝑠
21	20, 7	cfv 6525	. . . . . . . 8 class (Poly1‘𝑠)
22		vb	. . . . . . . . 9 setvar 𝑏
23		vg	. . . . . . . . . . . . 13 setvar 𝑔
24	23	cv 1562	. . . . . . . . . . . 12 class 𝑔
25	18	cv 1562	. . . . . . . . . . . . 13 class 𝑓
26	10, 25	ccom 5656	. . . . . . . . . . . 12 class (𝑝 ∘ 𝑓)
27	19	cv 1562	. . . . . . . . . . . . 13 class 𝑚
28		cdsr 20427	. . . . . . . . . . . . 13 class ∥r
29	27, 28	cfv 6525	. . . . . . . . . . . 12 class (∥r‘𝑚)
30	24, 26, 29	wbr 5105	. . . . . . . . . . 11 wff 𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓)
31	20, 24, 11	co 7400	. . . . . . . . . . . 12 class (𝑠deg1𝑔)
32		clt 11231	. . . . . . . . . . . 12 class <
33	9, 31, 32	wbr 5105	. . . . . . . . . . 11 wff 1 < (𝑠deg1𝑔)
34	30, 33	wa 400	. . . . . . . . . 10 wff (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))
35		cmn1 26244	. . . . . . . . . . . 12 class Monic1p
36	20, 35	cfv 6525	. . . . . . . . . . 11 class (Monic1p‘𝑠)
37		cir 20429	. . . . . . . . . . . 12 class Irred
38	27, 37	cfv 6525	. . . . . . . . . . 11 class (Irred‘𝑚)
39	36, 38	cin 3906	. . . . . . . . . 10 class ((Monic1p‘𝑠) ∩ (Irred‘𝑚))
40	34, 23, 39	crab 3417	. . . . . . . . 9 class {𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))}
41		c0g 17482	. . . . . . . . . . . . 13 class 0g
42	27, 41	cfv 6525	. . . . . . . . . . . 12 class (0g‘𝑚)
43	26, 42	wceq 1563	. . . . . . . . . . 11 wff (𝑝 ∘ 𝑓) = (0g‘𝑚)
44	22	cv 1562	. . . . . . . . . . . 12 class 𝑏
45		c0 4288	. . . . . . . . . . . 12 class ∅
46	44, 45	wceq 1563	. . . . . . . . . . 11 wff 𝑏 = ∅
47	43, 46	wo 860	. . . . . . . . . 10 wff ((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅)
48	20, 25	cop 4591	. . . . . . . . . 10 class ⟨𝑠, 𝑓⟩
49		vh	. . . . . . . . . . 11 setvar ℎ
50		cglb 18356	. . . . . . . . . . . 12 class glb
51	44, 50	cfv 6525	. . . . . . . . . . 11 class (glb‘𝑏)
52		vt	. . . . . . . . . . . 12 setvar 𝑡
53	49	cv 1562	. . . . . . . . . . . . 13 class ℎ
54		cpfl 35993	. . . . . . . . . . . . 13 class polyFld
55	20, 53, 54	co 7400	. . . . . . . . . . . 12 class (𝑠 polyFld ℎ)
56	52	cv 1562	. . . . . . . . . . . . . 14 class 𝑡
57		c1st 7972	. . . . . . . . . . . . . 14 class 1st
58	56, 57	cfv 6525	. . . . . . . . . . . . 13 class (1st ‘𝑡)
59		c2nd 7973	. . . . . . . . . . . . . . 15 class 2nd
60	56, 59	cfv 6525	. . . . . . . . . . . . . 14 class (2nd ‘𝑡)
61	25, 60	ccom 5656	. . . . . . . . . . . . 13 class (𝑓 ∘ (2nd ‘𝑡))
62	58, 61	cop 4591	. . . . . . . . . . . 12 class ⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
63	52, 55, 62	csb 3855	. . . . . . . . . . 11 class ⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
64	49, 51, 63	csb 3855	. . . . . . . . . 10 class ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
65	47, 48, 64	cif 4483	. . . . . . . . 9 class if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
66	22, 40, 65	csb 3855	. . . . . . . 8 class ⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
67	19, 21, 66	csb 3855	. . . . . . 7 class ⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
68	17, 18, 4, 4, 67	cmpo 7402	. . . . . 6 class (𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩))
69	3	cv 1562	. . . . . 6 class 𝑗
70	68, 69	crdg 8384	. . . . 5 class rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)), 𝑗)
71	16, 70	cfv 6525	. . . 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 5186	. . 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 7402	. 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 1563	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)