Definition df-sfl1 35631

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 35618	. 2 class splitFld1
2		vr	. . 3 setvar 𝑟
3		vj	. . 3 setvar 𝑗
4		cvv 3447	. . 3 class V
5		vp	. . . 4 setvar 𝑝
6	2	cv 1539	. . . . 5 class 𝑟
7		cpl1 22061	. . . . 5 class Poly1
8	6, 7	cfv 6511	. . . 4 class (Poly1‘𝑟)
9		c1 11069	. . . . . . 7 class 1
10	5	cv 1539	. . . . . . . 8 class 𝑝
11		cdg1 25959	. . . . . . . 8 class deg1
12	6, 10, 11	co 7387	. . . . . . 7 class (𝑟deg1𝑝)
13		cfz 13468	. . . . . . 7 class ...
14	9, 12, 13	co 7387	. . . . . 6 class (1...(𝑟deg1𝑝))
15		ccrd 9888	. . . . . 6 class card
16	14, 15	cfv 6511	. . . . 5 class (card‘(1...(𝑟deg1𝑝)))
17		vs	. . . . . . 7 setvar 𝑠
18		vf	. . . . . . 7 setvar 𝑓
19		vm	. . . . . . . 8 setvar 𝑚
20	17	cv 1539	. . . . . . . . 9 class 𝑠
21	20, 7	cfv 6511	. . . . . . . 8 class (Poly1‘𝑠)
22		vb	. . . . . . . . 9 setvar 𝑏
23		vg	. . . . . . . . . . . . 13 setvar 𝑔
24	23	cv 1539	. . . . . . . . . . . 12 class 𝑔
25	18	cv 1539	. . . . . . . . . . . . 13 class 𝑓
26	10, 25	ccom 5642	. . . . . . . . . . . 12 class (𝑝 ∘ 𝑓)
27	19	cv 1539	. . . . . . . . . . . . 13 class 𝑚
28		cdsr 20263	. . . . . . . . . . . . 13 class ∥r
29	27, 28	cfv 6511	. . . . . . . . . . . 12 class (∥r‘𝑚)
30	24, 26, 29	wbr 5107	. . . . . . . . . . 11 wff 𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓)
31	20, 24, 11	co 7387	. . . . . . . . . . . 12 class (𝑠deg1𝑔)
32		clt 11208	. . . . . . . . . . . 12 class <
33	9, 31, 32	wbr 5107	. . . . . . . . . . 11 wff 1 < (𝑠deg1𝑔)
34	30, 33	wa 395	. . . . . . . . . 10 wff (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))
35		cmn1 26031	. . . . . . . . . . . 12 class Monic1p
36	20, 35	cfv 6511	. . . . . . . . . . 11 class (Monic1p‘𝑠)
37		cir 20265	. . . . . . . . . . . 12 class Irred
38	27, 37	cfv 6511	. . . . . . . . . . 11 class (Irred‘𝑚)
39	36, 38	cin 3913	. . . . . . . . . 10 class ((Monic1p‘𝑠) ∩ (Irred‘𝑚))
40	34, 23, 39	crab 3405	. . . . . . . . 9 class {𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))}
41		c0g 17402	. . . . . . . . . . . . 13 class 0g
42	27, 41	cfv 6511	. . . . . . . . . . . 12 class (0g‘𝑚)
43	26, 42	wceq 1540	. . . . . . . . . . 11 wff (𝑝 ∘ 𝑓) = (0g‘𝑚)
44	22	cv 1539	. . . . . . . . . . . 12 class 𝑏
45		c0 4296	. . . . . . . . . . . 12 class ∅
46	44, 45	wceq 1540	. . . . . . . . . . 11 wff 𝑏 = ∅
47	43, 46	wo 847	. . . . . . . . . 10 wff ((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅)
48	20, 25	cop 4595	. . . . . . . . . 10 class ⟨𝑠, 𝑓⟩
49		vh	. . . . . . . . . . 11 setvar ℎ
50		cglb 18271	. . . . . . . . . . . 12 class glb
51	44, 50	cfv 6511	. . . . . . . . . . 11 class (glb‘𝑏)
52		vt	. . . . . . . . . . . 12 setvar 𝑡
53	49	cv 1539	. . . . . . . . . . . . 13 class ℎ
54		cpfl 35617	. . . . . . . . . . . . 13 class polyFld
55	20, 53, 54	co 7387	. . . . . . . . . . . 12 class (𝑠 polyFld ℎ)
56	52	cv 1539	. . . . . . . . . . . . . 14 class 𝑡
57		c1st 7966	. . . . . . . . . . . . . 14 class 1st
58	56, 57	cfv 6511	. . . . . . . . . . . . 13 class (1st ‘𝑡)
59		c2nd 7967	. . . . . . . . . . . . . . 15 class 2nd
60	56, 59	cfv 6511	. . . . . . . . . . . . . 14 class (2nd ‘𝑡)
61	25, 60	ccom 5642	. . . . . . . . . . . . 13 class (𝑓 ∘ (2nd ‘𝑡))
62	58, 61	cop 4595	. . . . . . . . . . . 12 class ⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
63	52, 55, 62	csb 3862	. . . . . . . . . . 11 class ⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
64	49, 51, 63	csb 3862	. . . . . . . . . 10 class ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
65	47, 48, 64	cif 4488	. . . . . . . . 9 class if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
66	22, 40, 65	csb 3862	. . . . . . . 8 class ⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
67	19, 21, 66	csb 3862	. . . . . . 7 class ⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
68	17, 18, 4, 4, 67	cmpo 7389	. . . . . 6 class (𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩))
69	3	cv 1539	. . . . . 6 class 𝑗
70	68, 69	crdg 8377	. . . . 5 class rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)), 𝑗)
71	16, 70	cfv 6511	. . . 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 5188	. . 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 7389	. 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 1540	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)