Definition df-sfl1 33581

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 ↦ ⦋( mPoly ‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((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 33573	. 2 class splitFld1
2		vr	. . 3 setvar 𝑟
3		vj	. . 3 setvar 𝑗
4		cvv 3430	. . 3 class V
5		vp	. . . 4 setvar 𝑝
6	2	cv 1540	. . . . 5 class 𝑟
7		cpl1 21329	. . . . 5 class Poly1
8	6, 7	cfv 6430	. . . 4 class (Poly1‘𝑟)
9		c1 10856	. . . . . . 7 class 1
10	5	cv 1540	. . . . . . . 8 class 𝑝
11		cdg1 25197	. . . . . . . 8 class deg1
12	6, 10, 11	co 7268	. . . . . . 7 class (𝑟 deg1 𝑝)
13		cfz 13221	. . . . . . 7 class ...
14	9, 12, 13	co 7268	. . . . . 6 class (1...(𝑟 deg1 𝑝))
15		ccrd 9677	. . . . . 6 class card
16	14, 15	cfv 6430	. . . . 5 class (card‘(1...(𝑟 deg1 𝑝)))
17		vs	. . . . . . 7 setvar 𝑠
18		vf	. . . . . . 7 setvar 𝑓
19		vm	. . . . . . . 8 setvar 𝑚
20	17	cv 1540	. . . . . . . . 9 class 𝑠
21		cmpl 21090	. . . . . . . . 9 class mPoly
22	20, 21	cfv 6430	. . . . . . . 8 class ( mPoly ‘𝑠)
23		vb	. . . . . . . . 9 setvar 𝑏
24		vg	. . . . . . . . . . . . 13 setvar 𝑔
25	24	cv 1540	. . . . . . . . . . . 12 class 𝑔
26	18	cv 1540	. . . . . . . . . . . . 13 class 𝑓
27	10, 26	ccom 5592	. . . . . . . . . . . 12 class (𝑝 ∘ 𝑓)
28	19	cv 1540	. . . . . . . . . . . . 13 class 𝑚
29		cdsr 19861	. . . . . . . . . . . . 13 class ∥r
30	28, 29	cfv 6430	. . . . . . . . . . . 12 class (∥r‘𝑚)
31	25, 27, 30	wbr 5078	. . . . . . . . . . 11 wff 𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓)
32	20, 25, 11	co 7268	. . . . . . . . . . . 12 class (𝑠 deg1 𝑔)
33		clt 10993	. . . . . . . . . . . 12 class <
34	9, 32, 33	wbr 5078	. . . . . . . . . . 11 wff 1 < (𝑠 deg1 𝑔)
35	31, 34	wa 395	. . . . . . . . . 10 wff (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))
36		cmn1 25271	. . . . . . . . . . . 12 class Monic1p
37	20, 36	cfv 6430	. . . . . . . . . . 11 class (Monic1p‘𝑠)
38		cir 19863	. . . . . . . . . . . 12 class Irred
39	28, 38	cfv 6430	. . . . . . . . . . 11 class (Irred‘𝑚)
40	37, 39	cin 3890	. . . . . . . . . 10 class ((Monic1p‘𝑠) ∩ (Irred‘𝑚))
41	35, 24, 40	crab 3069	. . . . . . . . 9 class {𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))}
42		c0g 17131	. . . . . . . . . . . . 13 class 0g
43	28, 42	cfv 6430	. . . . . . . . . . . 12 class (0g‘𝑚)
44	27, 43	wceq 1541	. . . . . . . . . . 11 wff (𝑝 ∘ 𝑓) = (0g‘𝑚)
45	23	cv 1540	. . . . . . . . . . . 12 class 𝑏
46		c0 4261	. . . . . . . . . . . 12 class ∅
47	45, 46	wceq 1541	. . . . . . . . . . 11 wff 𝑏 = ∅
48	44, 47	wo 843	. . . . . . . . . 10 wff ((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅)
49	20, 26	cop 4572	. . . . . . . . . 10 class ⟨𝑠, 𝑓⟩
50		vh	. . . . . . . . . . 11 setvar ℎ
51		cglb 18009	. . . . . . . . . . . 12 class glb
52	45, 51	cfv 6430	. . . . . . . . . . 11 class (glb‘𝑏)
53		vt	. . . . . . . . . . . 12 setvar 𝑡
54	50	cv 1540	. . . . . . . . . . . . 13 class ℎ
55		cpfl 33572	. . . . . . . . . . . . 13 class polyFld
56	20, 54, 55	co 7268	. . . . . . . . . . . 12 class (𝑠 polyFld ℎ)
57	53	cv 1540	. . . . . . . . . . . . . 14 class 𝑡
58		c1st 7815	. . . . . . . . . . . . . 14 class 1st
59	57, 58	cfv 6430	. . . . . . . . . . . . 13 class (1st ‘𝑡)
60		c2nd 7816	. . . . . . . . . . . . . . 15 class 2nd
61	57, 60	cfv 6430	. . . . . . . . . . . . . 14 class (2nd ‘𝑡)
62	26, 61	ccom 5592	. . . . . . . . . . . . 13 class (𝑓 ∘ (2nd ‘𝑡))
63	59, 62	cop 4572	. . . . . . . . . . . 12 class ⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
64	53, 56, 63	csb 3836	. . . . . . . . . . 11 class ⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
65	50, 52, 64	csb 3836	. . . . . . . . . 10 class ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
66	48, 49, 65	cif 4464	. . . . . . . . 9 class if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
67	23, 41, 66	csb 3836	. . . . . . . 8 class ⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
68	19, 22, 67	csb 3836	. . . . . . 7 class ⦋( mPoly ‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
69	17, 18, 4, 4, 68	cmpo 7270	. . . . . 6 class (𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋( mPoly ‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩))
70	3	cv 1540	. . . . . 6 class 𝑗
71	69, 70	crdg 8224	. . . . 5 class rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋( mPoly ‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)), 𝑗)
72	16, 71	cfv 6430	. . . 4 class (rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋( mPoly ‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)), 𝑗)‘(card‘(1...(𝑟 deg1 𝑝))))
73	5, 8, 72	cmpt 5161	. . 3 class (𝑝 ∈ (Poly1‘𝑟) ↦ (rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋( mPoly ‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)), 𝑗)‘(card‘(1...(𝑟 deg1 𝑝)))))
74	2, 3, 4, 4, 73	cmpo 7270	. 2 class (𝑟 ∈ V, 𝑗 ∈ V ↦ (𝑝 ∈ (Poly1‘𝑟) ↦ (rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋( mPoly ‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)), 𝑗)‘(card‘(1...(𝑟 deg1 𝑝))))))
75	1, 74	wceq 1541	1 wff splitFld1 = (𝑟 ∈ V, 𝑗 ∈ V ↦ (𝑝 ∈ (Poly1‘𝑟) ↦ (rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋( mPoly ‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)), 𝑗)‘(card‘(1...(𝑟 deg1 𝑝))))))

This definition is referenced by: (None)