Definition df-sfl1 32882

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 32874	. 2 class splitFld1
2		vr	. . 3 setvar 𝑟
3		vj	. . 3 setvar 𝑗
4		cvv 3494	. . 3 class V
5		vp	. . . 4 setvar 𝑝
6	2	cv 1532	. . . . 5 class 𝑟
7		cpl1 20339	. . . . 5 class Poly1
8	6, 7	cfv 6349	. . . 4 class (Poly1‘𝑟)
9		c1 10532	. . . . . . 7 class 1
10	5	cv 1532	. . . . . . . 8 class 𝑝
11		cdg1 24642	. . . . . . . 8 class deg1
12	6, 10, 11	co 7150	. . . . . . 7 class (𝑟 deg1 𝑝)
13		cfz 12886	. . . . . . 7 class ...
14	9, 12, 13	co 7150	. . . . . 6 class (1...(𝑟 deg1 𝑝))
15		ccrd 9358	. . . . . 6 class card
16	14, 15	cfv 6349	. . . . 5 class (card‘(1...(𝑟 deg1 𝑝)))
17		vs	. . . . . . 7 setvar 𝑠
18		vf	. . . . . . 7 setvar 𝑓
19		vm	. . . . . . . 8 setvar 𝑚
20	17	cv 1532	. . . . . . . . 9 class 𝑠
21		cmpl 20127	. . . . . . . . 9 class mPoly
22	20, 21	cfv 6349	. . . . . . . 8 class ( mPoly ‘𝑠)
23		vb	. . . . . . . . 9 setvar 𝑏
24		vg	. . . . . . . . . . . . 13 setvar 𝑔
25	24	cv 1532	. . . . . . . . . . . 12 class 𝑔
26	18	cv 1532	. . . . . . . . . . . . 13 class 𝑓
27	10, 26	ccom 5553	. . . . . . . . . . . 12 class (𝑝 ∘ 𝑓)
28	19	cv 1532	. . . . . . . . . . . . 13 class 𝑚
29		cdsr 19382	. . . . . . . . . . . . 13 class ∥r
30	28, 29	cfv 6349	. . . . . . . . . . . 12 class (∥r‘𝑚)
31	25, 27, 30	wbr 5058	. . . . . . . . . . 11 wff 𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓)
32	20, 25, 11	co 7150	. . . . . . . . . . . 12 class (𝑠 deg1 𝑔)
33		clt 10669	. . . . . . . . . . . 12 class <
34	9, 32, 33	wbr 5058	. . . . . . . . . . 11 wff 1 < (𝑠 deg1 𝑔)
35	31, 34	wa 398	. . . . . . . . . 10 wff (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))
36		cmn1 24713	. . . . . . . . . . . 12 class Monic1p
37	20, 36	cfv 6349	. . . . . . . . . . 11 class (Monic1p‘𝑠)
38		cir 19384	. . . . . . . . . . . 12 class Irred
39	28, 38	cfv 6349	. . . . . . . . . . 11 class (Irred‘𝑚)
40	37, 39	cin 3934	. . . . . . . . . 10 class ((Monic1p‘𝑠) ∩ (Irred‘𝑚))
41	35, 24, 40	crab 3142	. . . . . . . . 9 class {𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))}
42		c0g 16707	. . . . . . . . . . . . 13 class 0g
43	28, 42	cfv 6349	. . . . . . . . . . . 12 class (0g‘𝑚)
44	27, 43	wceq 1533	. . . . . . . . . . 11 wff (𝑝 ∘ 𝑓) = (0g‘𝑚)
45	23	cv 1532	. . . . . . . . . . . 12 class 𝑏
46		c0 4290	. . . . . . . . . . . 12 class ∅
47	45, 46	wceq 1533	. . . . . . . . . . 11 wff 𝑏 = ∅
48	44, 47	wo 843	. . . . . . . . . 10 wff ((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅)
49	20, 26	cop 4566	. . . . . . . . . 10 class ⟨𝑠, 𝑓⟩
50		vh	. . . . . . . . . . 11 setvar ℎ
51		cglb 17547	. . . . . . . . . . . 12 class glb
52	45, 51	cfv 6349	. . . . . . . . . . 11 class (glb‘𝑏)
53		vt	. . . . . . . . . . . 12 setvar 𝑡
54	50	cv 1532	. . . . . . . . . . . . 13 class ℎ
55		cpfl 32873	. . . . . . . . . . . . 13 class polyFld
56	20, 54, 55	co 7150	. . . . . . . . . . . 12 class (𝑠 polyFld ℎ)
57	53	cv 1532	. . . . . . . . . . . . . 14 class 𝑡
58		c1st 7681	. . . . . . . . . . . . . 14 class 1st
59	57, 58	cfv 6349	. . . . . . . . . . . . 13 class (1st ‘𝑡)
60		c2nd 7682	. . . . . . . . . . . . . . 15 class 2nd
61	57, 60	cfv 6349	. . . . . . . . . . . . . 14 class (2nd ‘𝑡)
62	26, 61	ccom 5553	. . . . . . . . . . . . 13 class (𝑓 ∘ (2nd ‘𝑡))
63	59, 62	cop 4566	. . . . . . . . . . . 12 class ⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
64	53, 56, 63	csb 3882	. . . . . . . . . . 11 class ⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
65	50, 52, 64	csb 3882	. . . . . . . . . 10 class ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
66	48, 49, 65	cif 4466	. . . . . . . . 9 class if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
67	23, 41, 66	csb 3882	. . . . . . . 8 class ⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
68	19, 22, 67	csb 3882	. . . . . . 7 class ⦋( mPoly ‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
69	17, 18, 4, 4, 68	cmpo 7152	. . . . . 6 class (𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋( mPoly ‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩))
70	3	cv 1532	. . . . . 6 class 𝑗
71	69, 70	crdg 8039	. . . . 5 class rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋( mPoly ‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)), 𝑗)
72	16, 71	cfv 6349	. . . 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 5138	. . 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 7152	. 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 1533	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)