Definition df-sfl1 36231

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 36218	. 2 class splitFld1
2		vr	. . 3 setvar 𝑟
3		vj	. . 3 setvar 𝑗
4		cvv 3453	. . 3 class V
5		vp	. . . 4 setvar 𝑝
6	2	cv 1569	. . . . 5 class 𝑟
7		cpl1 22408	. . . . 5 class Poly1
8	6, 7	cfv 6537	. . . 4 class (Poly1‘𝑟)
9		c1 11129	. . . . . . 7 class 1
10	5	cv 1569	. . . . . . . 8 class 𝑝
11		cdg1 26286	. . . . . . . 8 class deg1
12	6, 10, 11	co 7417	. . . . . . 7 class (𝑟deg1𝑝)
13		cfz 13565	. . . . . . 7 class ...
14	9, 12, 13	co 7417	. . . . . 6 class (1...(𝑟deg1𝑝))
15		ccrd 9944	. . . . . 6 class card
16	14, 15	cfv 6537	. . . . 5 class (card‘(1...(𝑟deg1𝑝)))
17		vs	. . . . . . 7 setvar 𝑠
18		vf	. . . . . . 7 setvar 𝑓
19		vm	. . . . . . . 8 setvar 𝑚
20	17	cv 1569	. . . . . . . . 9 class 𝑠
21	20, 7	cfv 6537	. . . . . . . 8 class (Poly1‘𝑠)
22		vb	. . . . . . . . 9 setvar 𝑏
23		vg	. . . . . . . . . . . . 13 setvar 𝑔
24	23	cv 1569	. . . . . . . . . . . 12 class 𝑔
25	18	cv 1569	. . . . . . . . . . . . 13 class 𝑓
26	10, 25	ccom 5663	. . . . . . . . . . . 12 class (𝑝 ∘ 𝑓)
27	19	cv 1569	. . . . . . . . . . . . 13 class 𝑚
28		cdsr 20501	. . . . . . . . . . . . 13 class ∥r
29	27, 28	cfv 6537	. . . . . . . . . . . 12 class (∥r‘𝑚)
30	24, 26, 29	wbr 5107	. . . . . . . . . . 11 wff 𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓)
31	20, 24, 11	co 7417	. . . . . . . . . . . 12 class (𝑠deg1𝑔)
32		clt 11271	. . . . . . . . . . . 12 class <
33	9, 31, 32	wbr 5107	. . . . . . . . . . 11 wff 1 < (𝑠deg1𝑔)
34	30, 33	wa 401	. . . . . . . . . 10 wff (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))
35		cmn1 26358	. . . . . . . . . . . 12 class Monic1p
36	20, 35	cfv 6537	. . . . . . . . . . 11 class (Monic1p‘𝑠)
37		cir 20503	. . . . . . . . . . . 12 class Irred
38	27, 37	cfv 6537	. . . . . . . . . . 11 class (Irred‘𝑚)
39	36, 38	cin 3901	. . . . . . . . . 10 class ((Monic1p‘𝑠) ∩ (Irred‘𝑚))
40	34, 23, 39	crab 3414	. . . . . . . . 9 class {𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))}
41		c0g 17530	. . . . . . . . . . . . 13 class 0g
42	27, 41	cfv 6537	. . . . . . . . . . . 12 class (0g‘𝑚)
43	26, 42	wceq 1570	. . . . . . . . . . 11 wff (𝑝 ∘ 𝑓) = (0g‘𝑚)
44	22	cv 1569	. . . . . . . . . . . 12 class 𝑏
45		c0 4282	. . . . . . . . . . . 12 class ∅
46	44, 45	wceq 1570	. . . . . . . . . . 11 wff 𝑏 = ∅
47	43, 46	wo 861	. . . . . . . . . 10 wff ((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅)
48	20, 25	cop 4593	. . . . . . . . . 10 class ⟨𝑠, 𝑓⟩
49		vh	. . . . . . . . . . 11 setvar ℎ
50		cglb 18404	. . . . . . . . . . . 12 class glb
51	44, 50	cfv 6537	. . . . . . . . . . 11 class (glb‘𝑏)
52		vt	. . . . . . . . . . . 12 setvar 𝑡
53	49	cv 1569	. . . . . . . . . . . . 13 class ℎ
54		cpfl 36217	. . . . . . . . . . . . 13 class polyFld
55	20, 53, 54	co 7417	. . . . . . . . . . . 12 class (𝑠 polyFld ℎ)
56	52	cv 1569	. . . . . . . . . . . . . 14 class 𝑡
57		c1st 7988	. . . . . . . . . . . . . 14 class 1st
58	56, 57	cfv 6537	. . . . . . . . . . . . 13 class (1st ‘𝑡)
59		c2nd 7989	. . . . . . . . . . . . . . 15 class 2nd
60	56, 59	cfv 6537	. . . . . . . . . . . . . 14 class (2nd ‘𝑡)
61	25, 60	ccom 5663	. . . . . . . . . . . . 13 class (𝑓 ∘ (2nd ‘𝑡))
62	58, 61	cop 4593	. . . . . . . . . . . 12 class ⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
63	52, 55, 62	csb 3850	. . . . . . . . . . 11 class ⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
64	49, 51, 63	csb 3850	. . . . . . . . . 10 class ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
65	47, 48, 64	cif 4485	. . . . . . . . 9 class if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
66	22, 40, 65	csb 3850	. . . . . . . 8 class ⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
67	19, 21, 66	csb 3850	. . . . . . 7 class ⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
68	17, 18, 4, 4, 67	cmpo 7419	. . . . . 6 class (𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩))
69	3	cv 1569	. . . . . 6 class 𝑗
70	68, 69	crdg 8402	. . . . 5 class rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)), 𝑗)
71	16, 70	cfv 6537	. . . 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 5190	. . 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 7419	. 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 1570	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 used by: (None)