Definition df-sfl1 34624

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 34617	. 2 class splitFld1
2		vr	. . 3 setvar 𝑟
3		vj	. . 3 setvar 𝑗
4		cvv 3474	. . 3 class V
5		vp	. . . 4 setvar 𝑝
6	2	cv 1540	. . . . 5 class 𝑟
7		cpl1 21700	. . . . 5 class Poly1
8	6, 7	cfv 6543	. . . 4 class (Poly1‘𝑟)
9		c1 11110	. . . . . . 7 class 1
10	5	cv 1540	. . . . . . . 8 class 𝑝
11		cdg1 25568	. . . . . . . 8 class deg1
12	6, 10, 11	co 7408	. . . . . . 7 class (𝑟 deg1 𝑝)
13		cfz 13483	. . . . . . 7 class ...
14	9, 12, 13	co 7408	. . . . . 6 class (1...(𝑟 deg1 𝑝))
15		ccrd 9929	. . . . . 6 class card
16	14, 15	cfv 6543	. . . . 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 21458	. . . . . . . . 9 class mPoly
22	20, 21	cfv 6543	. . . . . . . 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 5680	. . . . . . . . . . . 12 class (𝑝 ∘ 𝑓)
28	19	cv 1540	. . . . . . . . . . . . 13 class 𝑚
29		cdsr 20167	. . . . . . . . . . . . 13 class ∥r
30	28, 29	cfv 6543	. . . . . . . . . . . 12 class (∥r‘𝑚)
31	25, 27, 30	wbr 5148	. . . . . . . . . . 11 wff 𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓)
32	20, 25, 11	co 7408	. . . . . . . . . . . 12 class (𝑠 deg1 𝑔)
33		clt 11247	. . . . . . . . . . . 12 class <
34	9, 32, 33	wbr 5148	. . . . . . . . . . 11 wff 1 < (𝑠 deg1 𝑔)
35	31, 34	wa 396	. . . . . . . . . 10 wff (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))
36		cmn1 25642	. . . . . . . . . . . 12 class Monic1p
37	20, 36	cfv 6543	. . . . . . . . . . 11 class (Monic1p‘𝑠)
38		cir 20169	. . . . . . . . . . . 12 class Irred
39	28, 38	cfv 6543	. . . . . . . . . . 11 class (Irred‘𝑚)
40	37, 39	cin 3947	. . . . . . . . . 10 class ((Monic1p‘𝑠) ∩ (Irred‘𝑚))
41	35, 24, 40	crab 3432	. . . . . . . . 9 class {𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))}
42		c0g 17384	. . . . . . . . . . . . 13 class 0g
43	28, 42	cfv 6543	. . . . . . . . . . . 12 class (0g‘𝑚)
44	27, 43	wceq 1541	. . . . . . . . . . 11 wff (𝑝 ∘ 𝑓) = (0g‘𝑚)
45	23	cv 1540	. . . . . . . . . . . 12 class 𝑏
46		c0 4322	. . . . . . . . . . . 12 class ∅
47	45, 46	wceq 1541	. . . . . . . . . . 11 wff 𝑏 = ∅
48	44, 47	wo 845	. . . . . . . . . 10 wff ((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅)
49	20, 26	cop 4634	. . . . . . . . . 10 class ⟨𝑠, 𝑓⟩
50		vh	. . . . . . . . . . 11 setvar ℎ
51		cglb 18262	. . . . . . . . . . . 12 class glb
52	45, 51	cfv 6543	. . . . . . . . . . 11 class (glb‘𝑏)
53		vt	. . . . . . . . . . . 12 setvar 𝑡
54	50	cv 1540	. . . . . . . . . . . . 13 class ℎ
55		cpfl 34616	. . . . . . . . . . . . 13 class polyFld
56	20, 54, 55	co 7408	. . . . . . . . . . . 12 class (𝑠 polyFld ℎ)
57	53	cv 1540	. . . . . . . . . . . . . 14 class 𝑡
58		c1st 7972	. . . . . . . . . . . . . 14 class 1st
59	57, 58	cfv 6543	. . . . . . . . . . . . 13 class (1st ‘𝑡)
60		c2nd 7973	. . . . . . . . . . . . . . 15 class 2nd
61	57, 60	cfv 6543	. . . . . . . . . . . . . 14 class (2nd ‘𝑡)
62	26, 61	ccom 5680	. . . . . . . . . . . . 13 class (𝑓 ∘ (2nd ‘𝑡))
63	59, 62	cop 4634	. . . . . . . . . . . 12 class ⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
64	53, 56, 63	csb 3893	. . . . . . . . . . 11 class ⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
65	50, 52, 64	csb 3893	. . . . . . . . . 10 class ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
66	48, 49, 65	cif 4528	. . . . . . . . 9 class if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
67	23, 41, 66	csb 3893	. . . . . . . 8 class ⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
68	19, 22, 67	csb 3893	. . . . . . 7 class ⦋( mPoly ‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
69	17, 18, 4, 4, 68	cmpo 7410	. . . . . 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 8408	. . . . 5 class rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋( mPoly ‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)), 𝑗)
72	16, 71	cfv 6543	. . . 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 5231	. . 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 7410	. 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)