Definition df-sfl1 30789

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 30781	. 2 class splitFld1
2		vr	. . 3 setvar 𝑟
3		vj	. . 3 setvar 𝑗
4		cvv 3173	. . 3 class V
5		vp	. . . 4 setvar 𝑝
6	2	cv 1474	. . . . 5 class 𝑟
7		cpl1 19368	. . . . 5 class Poly1
8	6, 7	cfv 5804	. . . 4 class (Poly1‘𝑟)
9		c1 9816	. . . . . . 7 class 1
10	5	cv 1474	. . . . . . . 8 class 𝑝
11		cdg1 23618	. . . . . . . 8 class deg1
12	6, 10, 11	co 6549	. . . . . . 7 class (𝑟 deg1 𝑝)
13		cfz 12197	. . . . . . 7 class ...
14	9, 12, 13	co 6549	. . . . . 6 class (1...(𝑟 deg1 𝑝))
15		ccrd 8644	. . . . . 6 class card
16	14, 15	cfv 5804	. . . . 5 class (card‘(1...(𝑟 deg1 𝑝)))
17		vs	. . . . . . 7 setvar 𝑠
18		vf	. . . . . . 7 setvar 𝑓
19		vm	. . . . . . . 8 setvar 𝑚
20	17	cv 1474	. . . . . . . . 9 class 𝑠
21		cmpl 19174	. . . . . . . . 9 class mPoly
22	20, 21	cfv 5804	. . . . . . . 8 class ( mPoly ‘𝑠)
23		vb	. . . . . . . . 9 setvar 𝑏
24		vg	. . . . . . . . . . . . 13 setvar 𝑔
25	24	cv 1474	. . . . . . . . . . . 12 class 𝑔
26	18	cv 1474	. . . . . . . . . . . . 13 class 𝑓
27	10, 26	ccom 5042	. . . . . . . . . . . 12 class (𝑝 ∘ 𝑓)
28	19	cv 1474	. . . . . . . . . . . . 13 class 𝑚
29		cdsr 18461	. . . . . . . . . . . . 13 class ∥r
30	28, 29	cfv 5804	. . . . . . . . . . . 12 class (∥r‘𝑚)
31	25, 27, 30	wbr 4583	. . . . . . . . . . 11 wff 𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓)
32	20, 25, 11	co 6549	. . . . . . . . . . . 12 class (𝑠 deg1 𝑔)
33		clt 9953	. . . . . . . . . . . 12 class <
34	9, 32, 33	wbr 4583	. . . . . . . . . . 11 wff 1 < (𝑠 deg1 𝑔)
35	31, 34	wa 383	. . . . . . . . . 10 wff (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))
36		cmn1 23689	. . . . . . . . . . . 12 class Monic1p
37	20, 36	cfv 5804	. . . . . . . . . . 11 class (Monic1p‘𝑠)
38		cir 18463	. . . . . . . . . . . 12 class Irred
39	28, 38	cfv 5804	. . . . . . . . . . 11 class (Irred‘𝑚)
40	37, 39	cin 3539	. . . . . . . . . 10 class ((Monic1p‘𝑠) ∩ (Irred‘𝑚))
41	35, 24, 40	crab 2900	. . . . . . . . 9 class {𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))}
42		c0g 15923	. . . . . . . . . . . . 13 class 0g
43	28, 42	cfv 5804	. . . . . . . . . . . 12 class (0g‘𝑚)
44	27, 43	wceq 1475	. . . . . . . . . . 11 wff (𝑝 ∘ 𝑓) = (0g‘𝑚)
45	23	cv 1474	. . . . . . . . . . . 12 class 𝑏
46		c0 3874	. . . . . . . . . . . 12 class ∅
47	45, 46	wceq 1475	. . . . . . . . . . 11 wff 𝑏 = ∅
48	44, 47	wo 382	. . . . . . . . . 10 wff ((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅)
49	20, 26	cop 4131	. . . . . . . . . 10 class ⟨𝑠, 𝑓⟩
50		vh	. . . . . . . . . . 11 setvar ℎ
51		cglb 16766	. . . . . . . . . . . 12 class glb
52	45, 51	cfv 5804	. . . . . . . . . . 11 class (glb‘𝑏)
53		vt	. . . . . . . . . . . 12 setvar 𝑡
54	50	cv 1474	. . . . . . . . . . . . 13 class ℎ
55		cpfl 30780	. . . . . . . . . . . . 13 class polyFld
56	20, 54, 55	co 6549	. . . . . . . . . . . 12 class (𝑠 polyFld ℎ)
57	53	cv 1474	. . . . . . . . . . . . . 14 class 𝑡
58		c1st 7057	. . . . . . . . . . . . . 14 class 1st
59	57, 58	cfv 5804	. . . . . . . . . . . . 13 class (1st ‘𝑡)
60		c2nd 7058	. . . . . . . . . . . . . . 15 class 2nd
61	57, 60	cfv 5804	. . . . . . . . . . . . . 14 class (2nd ‘𝑡)
62	26, 61	ccom 5042	. . . . . . . . . . . . 13 class (𝑓 ∘ (2nd ‘𝑡))
63	59, 62	cop 4131	. . . . . . . . . . . 12 class ⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
64	53, 56, 63	csb 3499	. . . . . . . . . . 11 class ⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
65	50, 52, 64	csb 3499	. . . . . . . . . 10 class ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩
66	48, 49, 65	cif 4036	. . . . . . . . 9 class if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
67	23, 41, 66	csb 3499	. . . . . . . 8 class ⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
68	19, 22, 67	csb 3499	. . . . . . 7 class ⦋( mPoly ‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)
69	17, 18, 4, 4, 68	cmpt2 6551	. . . . . 6 class (𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋( mPoly ‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩))
70	3	cv 1474	. . . . . 6 class 𝑗
71	69, 70	crdg 7392	. . . . 5 class rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋( mPoly ‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)), 𝑗)
72	16, 71	cfv 5804	. . . 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 4643	. . 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	cmpt2 6551	. 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 1475	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)