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