Definition df-sfl1 35633

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 35620	. 2 class splitFld1
2		vr	. . 3 setvar 𝑟
3		vj	. . 3 setvar 𝑗
4		cvv 3455	. . 3 class V
5		vp	. . . 4 setvar 𝑝
6	2	cv 1539	. . . . 5 class 𝑟
7		cpl1 22067	. . . . 5 class Poly1
8	6, 7	cfv 6519	. . . 4 class (Poly1‘𝑟)
9		c1 11087	. . . . . . 7 class 1
10	5	cv 1539	. . . . . . . 8 class 𝑝
11		cdg1 25966	. . . . . . . 8 class deg1
12	6, 10, 11	co 7394	. . . . . . 7 class (𝑟deg1𝑝)
13		cfz 13481	. . . . . . 7 class ...
14	9, 12, 13	co 7394	. . . . . 6 class (1...(𝑟deg1𝑝))
15		ccrd 9906	. . . . . 6 class card
16	14, 15	cfv 6519	. . . . 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 6519	. . . . . . . 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 5650	. . . . . . . . . . . 12 class (𝑝 ∘ 𝑓)
27	19	cv 1539	. . . . . . . . . . . . 13 class 𝑚
28		cdsr 20269	. . . . . . . . . . . . 13 class ∥r
29	27, 28	cfv 6519	. . . . . . . . . . . 12 class (∥r‘𝑚)
30	24, 26, 29	wbr 5115	. . . . . . . . . . 11 wff 𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓)
31	20, 24, 11	co 7394	. . . . . . . . . . . 12 class (𝑠deg1𝑔)
32		clt 11226	. . . . . . . . . . . 12 class <
33	9, 31, 32	wbr 5115	. . . . . . . . . . 11 wff 1 < (𝑠deg1𝑔)
34	30, 33	wa 395	. . . . . . . . . 10 wff (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))
35		cmn1 26038	. . . . . . . . . . . 12 class Monic1p
36	20, 35	cfv 6519	. . . . . . . . . . 11 class (Monic1p‘𝑠)
37		cir 20271	. . . . . . . . . . . 12 class Irred
38	27, 37	cfv 6519	. . . . . . . . . . 11 class (Irred‘𝑚)
39	36, 38	cin 3921	. . . . . . . . . 10 class ((Monic1p‘𝑠) ∩ (Irred‘𝑚))
40	34, 23, 39	crab 3411	. . . . . . . . 9 class {𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))}
41		c0g 17408	. . . . . . . . . . . . 13 class 0g
42	27, 41	cfv 6519	. . . . . . . . . . . 12 class (0g‘𝑚)
43	26, 42	wceq 1540	. . . . . . . . . . 11 wff (𝑝 ∘ 𝑓) = (0g‘𝑚)
44	22	cv 1539	. . . . . . . . . . . 12 class 𝑏
45		c0 4304	. . . . . . . . . . . 12 class ∅
46	44, 45	wceq 1540	. . . . . . . . . . 11 wff 𝑏 = ∅
47	43, 46	wo 847	. . . . . . . . . 10 wff ((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅)
48	20, 25	cop 4603	. . . . . . . . . 10 class ⟨𝑠, 𝑓⟩
49		vh	. . . . . . . . . . 11 setvar ℎ
50		cglb 18277	. . . . . . . . . . . 12 class glb
51	44, 50	cfv 6519	. . . . . . . . . . 11 class (glb‘𝑏)
52		vt	. . . . . . . . . . . 12 setvar 𝑡
53	49	cv 1539	. . . . . . . . . . . . 13 class ℎ
54		cpfl 35619	. . . . . . . . . . . . 13 class polyFld
55	20, 53, 54	co 7394	. . . . . . . . . . . 12 class (𝑠 polyFld ℎ)
56	52	cv 1539	. . . . . . . . . . . . . 14 class 𝑡
57		c1st 7975	. . . . . . . . . . . . . 14 class 1st
58	56, 57	cfv 6519	. . . . . . . . . . . . 13 class (1st ‘𝑡)
59		c2nd 7976	. . . . . . . . . . . . . . 15 class 2nd
60	56, 59	cfv 6519	. . . . . . . . . . . . . 14 class (2nd ‘𝑡)
61	25, 60	ccom 5650	. . . . . . . . . . . . 13 class (𝑓 ∘ (2nd ‘𝑡))
62	58, 61	cop 4603	. . . . . . . . . . . 12 class ⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
63	52, 55, 62	csb 3870	. . . . . . . . . . 11 class ⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
64	49, 51, 63	csb 3870	. . . . . . . . . 10 class ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
65	47, 48, 64	cif 4496	. . . . . . . . 9 class if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
66	22, 40, 65	csb 3870	. . . . . . . 8 class ⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
67	19, 21, 66	csb 3870	. . . . . . 7 class ⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
68	17, 18, 4, 4, 67	cmpo 7396	. . . . . 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 8386	. . . . 5 class rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)), 𝑗)
71	16, 70	cfv 6519	. . . 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 5196	. . 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 7396	. 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)