Definition df-sfl1

Description: Temporary construction for the splitting field of a polynomial. The inputs are a field r and a polynomial p that we want to split, along with a tuple j in the same format as the output. The output is a tuple <. S , F >. where S is the splitting field and F is an injective homomorphism from the original field r .

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)

	Ref	Expression
Assertion	df-sfl1	⊢ splitFld1 = ( 𝑟 ∈ V , 𝑗 ∈ V ↦ ( 𝑝 ∈ ( Poly1 ‘ 𝑟 ) ↦ ( rec ( ( 𝑠 ∈ V , 𝑓 ∈ V ↦ ⦋ ( mPoly ‘ 𝑠 ) / 𝑚 ⦌ ⦋ { 𝑔 ∈ ( ( Monic1p ‘ 𝑠 ) ∩ ( Irred ‘ 𝑚 ) ) ∣ ( 𝑔 ( ∥r ‘ 𝑚 ) ( 𝑝 ∘ 𝑓 ) ∧ 1 < ( 𝑠 deg1 𝑔 ) ) } / 𝑏 ⦌ if ( ( ( 𝑝 ∘ 𝑓 ) = ( 0g ‘ 𝑚 ) ∨ 𝑏 = ∅ ) , ⟨ 𝑠 , 𝑓 ⟩ , ⦋ ( glb ‘ 𝑏 ) / ℎ ⦌ ⦋ ( 𝑠 polyFld ℎ ) / 𝑡 ⦌ ⟨ ( 1st ‘ 𝑡 ) , ( 𝑓 ∘ ( 2nd ‘ 𝑡 ) ) ⟩ ) ) , 𝑗 ) ‘ ( card ‘ ( 1 ... ( 𝑟 deg1 𝑝 ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csf1	⊢ splitFld1
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		vj	⊢ 𝑗
4		vp	⊢ 𝑝
5		cpl1	⊢ Poly1
6	1	cv	⊢ 𝑟
7	6 5	cfv	⊢ ( Poly1 ‘ 𝑟 )
8		vs	⊢ 𝑠
9		vf	⊢ 𝑓
10		cmpl	⊢ mPoly
11	8	cv	⊢ 𝑠
12	11 10	cfv	⊢ ( mPoly ‘ 𝑠 )
13		vm	⊢ 𝑚
14		vg	⊢ 𝑔
15		cmn1	⊢ Monic1p
16	11 15	cfv	⊢ ( Monic1p ‘ 𝑠 )
17		cir	⊢ Irred
18	13	cv	⊢ 𝑚
19	18 17	cfv	⊢ ( Irred ‘ 𝑚 )
20	16 19	cin	⊢ ( ( Monic1p ‘ 𝑠 ) ∩ ( Irred ‘ 𝑚 ) )
21	14	cv	⊢ 𝑔
22		cdsr	⊢ ∥r
23	18 22	cfv	⊢ ( ∥r ‘ 𝑚 )
24	4	cv	⊢ 𝑝
25	9	cv	⊢ 𝑓
26	24 25	ccom	⊢ ( 𝑝 ∘ 𝑓 )
27	21 26 23	wbr	⊢ 𝑔 ( ∥r ‘ 𝑚 ) ( 𝑝 ∘ 𝑓 )
28		c1	⊢ 1
29		clt	⊢ <
30		cdg1	⊢ deg1
31	11 21 30	co	⊢ ( 𝑠 deg1 𝑔 )
32	28 31 29	wbr	⊢ 1 < ( 𝑠 deg1 𝑔 )
33	27 32	wa	⊢ ( 𝑔 ( ∥r ‘ 𝑚 ) ( 𝑝 ∘ 𝑓 ) ∧ 1 < ( 𝑠 deg1 𝑔 ) )
34	33 14 20	crab	⊢ { 𝑔 ∈ ( ( Monic1p ‘ 𝑠 ) ∩ ( Irred ‘ 𝑚 ) ) ∣ ( 𝑔 ( ∥r ‘ 𝑚 ) ( 𝑝 ∘ 𝑓 ) ∧ 1 < ( 𝑠 deg1 𝑔 ) ) }
35		vb	⊢ 𝑏
36		c0g	⊢ 0g
37	18 36	cfv	⊢ ( 0g ‘ 𝑚 )
38	26 37	wceq	⊢ ( 𝑝 ∘ 𝑓 ) = ( 0g ‘ 𝑚 )
39	35	cv	⊢ 𝑏
40		c0	⊢ ∅
41	39 40	wceq	⊢ 𝑏 = ∅
42	38 41	wo	⊢ ( ( 𝑝 ∘ 𝑓 ) = ( 0g ‘ 𝑚 ) ∨ 𝑏 = ∅ )
43	11 25	cop	⊢ ⟨ 𝑠 , 𝑓 ⟩
44		cglb	⊢ glb
45	39 44	cfv	⊢ ( glb ‘ 𝑏 )
46		vh	⊢ ℎ
47		cpfl	⊢ polyFld
48	46	cv	⊢ ℎ
49	11 48 47	co	⊢ ( 𝑠 polyFld ℎ )
50		vt	⊢ 𝑡
51		c1st	⊢ 1st
52	50	cv	⊢ 𝑡
53	52 51	cfv	⊢ ( 1st ‘ 𝑡 )
54		c2nd	⊢ 2nd
55	52 54	cfv	⊢ ( 2nd ‘ 𝑡 )
56	25 55	ccom	⊢ ( 𝑓 ∘ ( 2nd ‘ 𝑡 ) )
57	53 56	cop	⊢ ⟨ ( 1st ‘ 𝑡 ) , ( 𝑓 ∘ ( 2nd ‘ 𝑡 ) ) ⟩
58	50 49 57	csb	⊢ ⦋ ( 𝑠 polyFld ℎ ) / 𝑡 ⦌ ⟨ ( 1st ‘ 𝑡 ) , ( 𝑓 ∘ ( 2nd ‘ 𝑡 ) ) ⟩
59	46 45 58	csb	⊢ ⦋ ( glb ‘ 𝑏 ) / ℎ ⦌ ⦋ ( 𝑠 polyFld ℎ ) / 𝑡 ⦌ ⟨ ( 1st ‘ 𝑡 ) , ( 𝑓 ∘ ( 2nd ‘ 𝑡 ) ) ⟩
60	42 43 59	cif	⊢ if ( ( ( 𝑝 ∘ 𝑓 ) = ( 0g ‘ 𝑚 ) ∨ 𝑏 = ∅ ) , ⟨ 𝑠 , 𝑓 ⟩ , ⦋ ( glb ‘ 𝑏 ) / ℎ ⦌ ⦋ ( 𝑠 polyFld ℎ ) / 𝑡 ⦌ ⟨ ( 1st ‘ 𝑡 ) , ( 𝑓 ∘ ( 2nd ‘ 𝑡 ) ) ⟩ )
61	35 34 60	csb	⊢ ⦋ { 𝑔 ∈ ( ( Monic1p ‘ 𝑠 ) ∩ ( Irred ‘ 𝑚 ) ) ∣ ( 𝑔 ( ∥r ‘ 𝑚 ) ( 𝑝 ∘ 𝑓 ) ∧ 1 < ( 𝑠 deg1 𝑔 ) ) } / 𝑏 ⦌ if ( ( ( 𝑝 ∘ 𝑓 ) = ( 0g ‘ 𝑚 ) ∨ 𝑏 = ∅ ) , ⟨ 𝑠 , 𝑓 ⟩ , ⦋ ( glb ‘ 𝑏 ) / ℎ ⦌ ⦋ ( 𝑠 polyFld ℎ ) / 𝑡 ⦌ ⟨ ( 1st ‘ 𝑡 ) , ( 𝑓 ∘ ( 2nd ‘ 𝑡 ) ) ⟩ )
62	13 12 61	csb	⊢ ⦋ ( mPoly ‘ 𝑠 ) / 𝑚 ⦌ ⦋ { 𝑔 ∈ ( ( Monic1p ‘ 𝑠 ) ∩ ( Irred ‘ 𝑚 ) ) ∣ ( 𝑔 ( ∥r ‘ 𝑚 ) ( 𝑝 ∘ 𝑓 ) ∧ 1 < ( 𝑠 deg1 𝑔 ) ) } / 𝑏 ⦌ if ( ( ( 𝑝 ∘ 𝑓 ) = ( 0g ‘ 𝑚 ) ∨ 𝑏 = ∅ ) , ⟨ 𝑠 , 𝑓 ⟩ , ⦋ ( glb ‘ 𝑏 ) / ℎ ⦌ ⦋ ( 𝑠 polyFld ℎ ) / 𝑡 ⦌ ⟨ ( 1st ‘ 𝑡 ) , ( 𝑓 ∘ ( 2nd ‘ 𝑡 ) ) ⟩ )
63	8 9 2 2 62	cmpo	⊢ ( 𝑠 ∈ V , 𝑓 ∈ V ↦ ⦋ ( mPoly ‘ 𝑠 ) / 𝑚 ⦌ ⦋ { 𝑔 ∈ ( ( Monic1p ‘ 𝑠 ) ∩ ( Irred ‘ 𝑚 ) ) ∣ ( 𝑔 ( ∥r ‘ 𝑚 ) ( 𝑝 ∘ 𝑓 ) ∧ 1 < ( 𝑠 deg1 𝑔 ) ) } / 𝑏 ⦌ if ( ( ( 𝑝 ∘ 𝑓 ) = ( 0g ‘ 𝑚 ) ∨ 𝑏 = ∅ ) , ⟨ 𝑠 , 𝑓 ⟩ , ⦋ ( glb ‘ 𝑏 ) / ℎ ⦌ ⦋ ( 𝑠 polyFld ℎ ) / 𝑡 ⦌ ⟨ ( 1st ‘ 𝑡 ) , ( 𝑓 ∘ ( 2nd ‘ 𝑡 ) ) ⟩ ) )
64	3	cv	⊢ 𝑗
65	63 64	crdg	⊢ rec ( ( 𝑠 ∈ V , 𝑓 ∈ V ↦ ⦋ ( mPoly ‘ 𝑠 ) / 𝑚 ⦌ ⦋ { 𝑔 ∈ ( ( Monic1p ‘ 𝑠 ) ∩ ( Irred ‘ 𝑚 ) ) ∣ ( 𝑔 ( ∥r ‘ 𝑚 ) ( 𝑝 ∘ 𝑓 ) ∧ 1 < ( 𝑠 deg1 𝑔 ) ) } / 𝑏 ⦌ if ( ( ( 𝑝 ∘ 𝑓 ) = ( 0g ‘ 𝑚 ) ∨ 𝑏 = ∅ ) , ⟨ 𝑠 , 𝑓 ⟩ , ⦋ ( glb ‘ 𝑏 ) / ℎ ⦌ ⦋ ( 𝑠 polyFld ℎ ) / 𝑡 ⦌ ⟨ ( 1st ‘ 𝑡 ) , ( 𝑓 ∘ ( 2nd ‘ 𝑡 ) ) ⟩ ) ) , 𝑗 )
66		ccrd	⊢ card
67		cfz	⊢ ...
68	6 24 30	co	⊢ ( 𝑟 deg1 𝑝 )
69	28 68 67	co	⊢ ( 1 ... ( 𝑟 deg1 𝑝 ) )
70	69 66	cfv	⊢ ( card ‘ ( 1 ... ( 𝑟 deg1 𝑝 ) ) )
71	70 65	cfv	⊢ ( rec ( ( 𝑠 ∈ V , 𝑓 ∈ V ↦ ⦋ ( mPoly ‘ 𝑠 ) / 𝑚 ⦌ ⦋ { 𝑔 ∈ ( ( Monic1p ‘ 𝑠 ) ∩ ( Irred ‘ 𝑚 ) ) ∣ ( 𝑔 ( ∥r ‘ 𝑚 ) ( 𝑝 ∘ 𝑓 ) ∧ 1 < ( 𝑠 deg1 𝑔 ) ) } / 𝑏 ⦌ if ( ( ( 𝑝 ∘ 𝑓 ) = ( 0g ‘ 𝑚 ) ∨ 𝑏 = ∅ ) , ⟨ 𝑠 , 𝑓 ⟩ , ⦋ ( glb ‘ 𝑏 ) / ℎ ⦌ ⦋ ( 𝑠 polyFld ℎ ) / 𝑡 ⦌ ⟨ ( 1st ‘ 𝑡 ) , ( 𝑓 ∘ ( 2nd ‘ 𝑡 ) ) ⟩ ) ) , 𝑗 ) ‘ ( card ‘ ( 1 ... ( 𝑟 deg1 𝑝 ) ) ) )
72	4 7 71	cmpt	⊢ ( 𝑝 ∈ ( Poly1 ‘ 𝑟 ) ↦ ( rec ( ( 𝑠 ∈ V , 𝑓 ∈ V ↦ ⦋ ( mPoly ‘ 𝑠 ) / 𝑚 ⦌ ⦋ { 𝑔 ∈ ( ( Monic1p ‘ 𝑠 ) ∩ ( Irred ‘ 𝑚 ) ) ∣ ( 𝑔 ( ∥r ‘ 𝑚 ) ( 𝑝 ∘ 𝑓 ) ∧ 1 < ( 𝑠 deg1 𝑔 ) ) } / 𝑏 ⦌ if ( ( ( 𝑝 ∘ 𝑓 ) = ( 0g ‘ 𝑚 ) ∨ 𝑏 = ∅ ) , ⟨ 𝑠 , 𝑓 ⟩ , ⦋ ( glb ‘ 𝑏 ) / ℎ ⦌ ⦋ ( 𝑠 polyFld ℎ ) / 𝑡 ⦌ ⟨ ( 1st ‘ 𝑡 ) , ( 𝑓 ∘ ( 2nd ‘ 𝑡 ) ) ⟩ ) ) , 𝑗 ) ‘ ( card ‘ ( 1 ... ( 𝑟 deg1 𝑝 ) ) ) ) )
73	1 3 2 2 72	cmpo	⊢ ( 𝑟 ∈ V , 𝑗 ∈ V ↦ ( 𝑝 ∈ ( Poly1 ‘ 𝑟 ) ↦ ( rec ( ( 𝑠 ∈ V , 𝑓 ∈ V ↦ ⦋ ( mPoly ‘ 𝑠 ) / 𝑚 ⦌ ⦋ { 𝑔 ∈ ( ( Monic1p ‘ 𝑠 ) ∩ ( Irred ‘ 𝑚 ) ) ∣ ( 𝑔 ( ∥r ‘ 𝑚 ) ( 𝑝 ∘ 𝑓 ) ∧ 1 < ( 𝑠 deg1 𝑔 ) ) } / 𝑏 ⦌ if ( ( ( 𝑝 ∘ 𝑓 ) = ( 0g ‘ 𝑚 ) ∨ 𝑏 = ∅ ) , ⟨ 𝑠 , 𝑓 ⟩ , ⦋ ( glb ‘ 𝑏 ) / ℎ ⦌ ⦋ ( 𝑠 polyFld ℎ ) / 𝑡 ⦌ ⟨ ( 1st ‘ 𝑡 ) , ( 𝑓 ∘ ( 2nd ‘ 𝑡 ) ) ⟩ ) ) , 𝑗 ) ‘ ( card ‘ ( 1 ... ( 𝑟 deg1 𝑝 ) ) ) ) ) )
74	0 73	wceq	⊢ splitFld1 = ( 𝑟 ∈ V , 𝑗 ∈ V ↦ ( 𝑝 ∈ ( Poly1 ‘ 𝑟 ) ↦ ( rec ( ( 𝑠 ∈ V , 𝑓 ∈ V ↦ ⦋ ( mPoly ‘ 𝑠 ) / 𝑚 ⦌ ⦋ { 𝑔 ∈ ( ( Monic1p ‘ 𝑠 ) ∩ ( Irred ‘ 𝑚 ) ) ∣ ( 𝑔 ( ∥r ‘ 𝑚 ) ( 𝑝 ∘ 𝑓 ) ∧ 1 < ( 𝑠 deg1 𝑔 ) ) } / 𝑏 ⦌ if ( ( ( 𝑝 ∘ 𝑓 ) = ( 0g ‘ 𝑚 ) ∨ 𝑏 = ∅ ) , ⟨ 𝑠 , 𝑓 ⟩ , ⦋ ( glb ‘ 𝑏 ) / ℎ ⦌ ⦋ ( 𝑠 polyFld ℎ ) / 𝑡 ⦌ ⟨ ( 1st ‘ 𝑡 ) , ( 𝑓 ∘ ( 2nd ‘ 𝑡 ) ) ⟩ ) ) , 𝑗 ) ‘ ( card ‘ ( 1 ... ( 𝑟 deg1 𝑝 ) ) ) ) ) )