Definition df-sfl1 32894

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 32886	. 2 class splitFld1
2		vr	. . 3 setvar 𝑟
3		vj	. . 3 setvar 𝑗
4		cvv 3486	. . 3 class V
5		vp	. . . 4 setvar 𝑝
6	2	cv 1536	. . . . 5 class 𝑟
7		cpl1 20328	. . . . 5 class Poly1
8	6, 7	cfv 6341	. . . 4 class (Poly1‘𝑟)
9		c1 10524	. . . . . . 7 class 1
10	5	cv 1536	. . . . . . . 8 class 𝑝
11		cdg1 24634	. . . . . . . 8 class deg1
12	6, 10, 11	co 7142	. . . . . . 7 class (𝑟 deg1 𝑝)
13		cfz 12882	. . . . . . 7 class ...
14	9, 12, 13	co 7142	. . . . . 6 class (1...(𝑟 deg1 𝑝))
15		ccrd 9350	. . . . . 6 class card
16	14, 15	cfv 6341	. . . . 5 class (card‘(1...(𝑟 deg1 𝑝)))
17		vs	. . . . . . 7 setvar 𝑠
18		vf	. . . . . . 7 setvar 𝑓
19		vm	. . . . . . . 8 setvar 𝑚
20	17	cv 1536	. . . . . . . . 9 class 𝑠
21		cmpl 20116	. . . . . . . . 9 class mPoly
22	20, 21	cfv 6341	. . . . . . . 8 class ( mPoly ‘𝑠)
23		vb	. . . . . . . . 9 setvar 𝑏
24		vg	. . . . . . . . . . . . 13 setvar 𝑔
25	24	cv 1536	. . . . . . . . . . . 12 class 𝑔
26	18	cv 1536	. . . . . . . . . . . . 13 class 𝑓
27	10, 26	ccom 5545	. . . . . . . . . . . 12 class (𝑝 ∘ 𝑓)
28	19	cv 1536	. . . . . . . . . . . . 13 class 𝑚
29		cdsr 19371	. . . . . . . . . . . . 13 class ∥r
30	28, 29	cfv 6341	. . . . . . . . . . . 12 class (∥r‘𝑚)
31	25, 27, 30	wbr 5052	. . . . . . . . . . 11 wff 𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓)
32	20, 25, 11	co 7142	. . . . . . . . . . . 12 class (𝑠 deg1 𝑔)
33		clt 10661	. . . . . . . . . . . 12 class <
34	9, 32, 33	wbr 5052	. . . . . . . . . . 11 wff 1 < (𝑠 deg1 𝑔)
35	31, 34	wa 398	. . . . . . . . . 10 wff (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))
36		cmn1 24705	. . . . . . . . . . . 12 class Monic1p
37	20, 36	cfv 6341	. . . . . . . . . . 11 class (Monic1p‘𝑠)
38		cir 19373	. . . . . . . . . . . 12 class Irred
39	28, 38	cfv 6341	. . . . . . . . . . 11 class (Irred‘𝑚)
40	37, 39	cin 3923	. . . . . . . . . 10 class ((Monic1p‘𝑠) ∩ (Irred‘𝑚))
41	35, 24, 40	crab 3142	. . . . . . . . 9 class {𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))}
42		c0g 16696	. . . . . . . . . . . . 13 class 0g
43	28, 42	cfv 6341	. . . . . . . . . . . 12 class (0g‘𝑚)
44	27, 43	wceq 1537	. . . . . . . . . . 11 wff (𝑝 ∘ 𝑓) = (0g‘𝑚)
45	23	cv 1536	. . . . . . . . . . . 12 class 𝑏
46		c0 4279	. . . . . . . . . . . 12 class ∅
47	45, 46	wceq 1537	. . . . . . . . . . 11 wff 𝑏 = ∅
48	44, 47	wo 843	. . . . . . . . . 10 wff ((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅)
49	20, 26	cop 4559	. . . . . . . . . 10 class ⟨𝑠, 𝑓⟩
50		vh	. . . . . . . . . . 11 setvar ℎ
51		cglb 17536	. . . . . . . . . . . 12 class glb
52	45, 51	cfv 6341	. . . . . . . . . . 11 class (glb‘𝑏)
53		vt	. . . . . . . . . . . 12 setvar 𝑡
54	50	cv 1536	. . . . . . . . . . . . 13 class ℎ
55		cpfl 32885	. . . . . . . . . . . . 13 class polyFld
56	20, 54, 55	co 7142	. . . . . . . . . . . 12 class (𝑠 polyFld ℎ)
57	53	cv 1536	. . . . . . . . . . . . . 14 class 𝑡
58		c1st 7673	. . . . . . . . . . . . . 14 class 1st
59	57, 58	cfv 6341	. . . . . . . . . . . . 13 class (1st ‘𝑡)
60		c2nd 7674	. . . . . . . . . . . . . . 15 class 2nd
61	57, 60	cfv 6341	. . . . . . . . . . . . . 14 class (2nd ‘𝑡)
62	26, 61	ccom 5545	. . . . . . . . . . . . 13 class (𝑓 ∘ (2nd ‘𝑡))
63	59, 62	cop 4559	. . . . . . . . . . . 12 class ⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
64	53, 56, 63	csb 3871	. . . . . . . . . . 11 class ⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
65	50, 52, 64	csb 3871	. . . . . . . . . 10 class ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
66	48, 49, 65	cif 4453	. . . . . . . . 9 class if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
67	23, 41, 66	csb 3871	. . . . . . . 8 class ⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
68	19, 22, 67	csb 3871	. . . . . . 7 class ⦋( mPoly ‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
69	17, 18, 4, 4, 68	cmpo 7144	. . . . . 6 class (𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋( mPoly ‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩))
70	3	cv 1536	. . . . . 6 class 𝑗
71	69, 70	crdg 8031	. . . . 5 class rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋( mPoly ‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)), 𝑗)
72	16, 71	cfv 6341	. . . 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 5132	. . 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 7144	. 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 1537	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)