Metamath Proof Explorer

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 ⊢ splitFld 1 = r ∈ V , j ∈ V ⟼ p ∈ Poly 1 ⁡ r ⟼ rec ⁡ s ∈ V , f ∈ V ⟼ ⦋ mPoly ⁡ s / m⦌ ⦋ g ∈ Monic 1p ⁡ s ∩ Irred ⁡ m | g ∥ r ⁡ m p ∘ f ∧ 1 < s deg 1 g / b⦌ if p ∘ f = 0 m ∨ b = ∅ s f ⦋ glb ⁡ b / h⦌ ⦋ s polyFld h / t⦌ 1 st ⁡ t f ∘ 2 nd ⁡ t j ⁡ card ⁡ 1 … r deg 1 p

Detailed syntax breakdown

Step Hyp Ref Expression
0 csf1 class splitFld 1
1 vr setvar r
2 cvv class V
3 vj setvar j
4 vp setvar p
5 cpl1 class Poly 1
6 1 cv setvar r
7 6 5 cfv class Poly 1 ⁡ r
8 vs setvar s
9 vf setvar f
10 cmpl class mPoly
11 8 cv setvar s
12 11 10 cfv class mPoly ⁡ s
13 vm setvar m
14 vg setvar g
15 cmn1 class Monic 1p
16 11 15 cfv class Monic 1p ⁡ s
17 cir class Irred
18 13 cv setvar m
19 18 17 cfv class Irred ⁡ m
20 16 19 cin class Monic 1p ⁡ s ∩ Irred ⁡ m
21 14 cv setvar g
22 cdsr class ∥ r
23 18 22 cfv class ∥ r ⁡ m
24 4 cv setvar p
25 9 cv setvar f
26 24 25 ccom class p ∘ f
27 21 26 23 wbr wff g ∥ r ⁡ m p ∘ f
28 c1 class 1
29 clt class <
30 cdg1 class deg 1
31 11 21 30 co class s deg 1 g
32 28 31 29 wbr wff 1 < s deg 1 g
33 27 32 wa wff g ∥ r ⁡ m p ∘ f ∧ 1 < s deg 1 g
34 33 14 20 crab class g ∈ Monic 1p ⁡ s ∩ Irred ⁡ m | g ∥ r ⁡ m p ∘ f ∧ 1 < s deg 1 g
35 vb setvar b
36 c0g class 0 𝑔
37 18 36 cfv class 0 m
38 26 37 wceq wff p ∘ f = 0 m
39 35 cv setvar b
40 c0 class ∅
41 39 40 wceq wff b = ∅
42 38 41 wo wff p ∘ f = 0 m ∨ b = ∅
43 11 25 cop class s f
44 cglb class glb
45 39 44 cfv class glb ⁡ b
46 vh setvar h
47 cpfl class polyFld
48 46 cv setvar h
49 11 48 47 co class s polyFld h
50 vt setvar t
51 c1st class 1 st
52 50 cv setvar t
53 52 51 cfv class 1 st ⁡ t
54 c2nd class 2 nd
55 52 54 cfv class 2 nd ⁡ t
56 25 55 ccom class f ∘ 2 nd ⁡ t
57 53 56 cop class 1 st ⁡ t f ∘ 2 nd ⁡ t
58 50 49 57 csb class ⦋ s polyFld h / t⦌ 1 st ⁡ t f ∘ 2 nd ⁡ t
59 46 45 58 csb class ⦋ glb ⁡ b / h⦌ ⦋ s polyFld h / t⦌ 1 st ⁡ t f ∘ 2 nd ⁡ t
60 42 43 59 cif class if p ∘ f = 0 m ∨ b = ∅ s f ⦋ glb ⁡ b / h⦌ ⦋ s polyFld h / t⦌ 1 st ⁡ t f ∘ 2 nd ⁡ t
61 35 34 60 csb class ⦋ g ∈ Monic 1p ⁡ s ∩ Irred ⁡ m | g ∥ r ⁡ m p ∘ f ∧ 1 < s deg 1 g / b⦌ if p ∘ f = 0 m ∨ b = ∅ s f ⦋ glb ⁡ b / h⦌ ⦋ s polyFld h / t⦌ 1 st ⁡ t f ∘ 2 nd ⁡ t
62 13 12 61 csb class ⦋ mPoly ⁡ s / m⦌ ⦋ g ∈ Monic 1p ⁡ s ∩ Irred ⁡ m | g ∥ r ⁡ m p ∘ f ∧ 1 < s deg 1 g / b⦌ if p ∘ f = 0 m ∨ b = ∅ s f ⦋ glb ⁡ b / h⦌ ⦋ s polyFld h / t⦌ 1 st ⁡ t f ∘ 2 nd ⁡ t
63 8 9 2 2 62 cmpo class s ∈ V , f ∈ V ⟼ ⦋ mPoly ⁡ s / m⦌ ⦋ g ∈ Monic 1p ⁡ s ∩ Irred ⁡ m | g ∥ r ⁡ m p ∘ f ∧ 1 < s deg 1 g / b⦌ if p ∘ f = 0 m ∨ b = ∅ s f ⦋ glb ⁡ b / h⦌ ⦋ s polyFld h / t⦌ 1 st ⁡ t f ∘ 2 nd ⁡ t
64 3 cv setvar j
65 63 64 crdg class rec ⁡ s ∈ V , f ∈ V ⟼ ⦋ mPoly ⁡ s / m⦌ ⦋ g ∈ Monic 1p ⁡ s ∩ Irred ⁡ m | g ∥ r ⁡ m p ∘ f ∧ 1 < s deg 1 g / b⦌ if p ∘ f = 0 m ∨ b = ∅ s f ⦋ glb ⁡ b / h⦌ ⦋ s polyFld h / t⦌ 1 st ⁡ t f ∘ 2 nd ⁡ t j
66 ccrd class card
67 cfz class …
68 6 24 30 co class r deg 1 p
69 28 68 67 co class 1 … r deg 1 p
70 69 66 cfv class card ⁡ 1 … r deg 1 p
71 70 65 cfv class rec ⁡ s ∈ V , f ∈ V ⟼ ⦋ mPoly ⁡ s / m⦌ ⦋ g ∈ Monic 1p ⁡ s ∩ Irred ⁡ m | g ∥ r ⁡ m p ∘ f ∧ 1 < s deg 1 g / b⦌ if p ∘ f = 0 m ∨ b = ∅ s f ⦋ glb ⁡ b / h⦌ ⦋ s polyFld h / t⦌ 1 st ⁡ t f ∘ 2 nd ⁡ t j ⁡ card ⁡ 1 … r deg 1 p
72 4 7 71 cmpt class p ∈ Poly 1 ⁡ r ⟼ rec ⁡ s ∈ V , f ∈ V ⟼ ⦋ mPoly ⁡ s / m⦌ ⦋ g ∈ Monic 1p ⁡ s ∩ Irred ⁡ m | g ∥ r ⁡ m p ∘ f ∧ 1 < s deg 1 g / b⦌ if p ∘ f = 0 m ∨ b = ∅ s f ⦋ glb ⁡ b / h⦌ ⦋ s polyFld h / t⦌ 1 st ⁡ t f ∘ 2 nd ⁡ t j ⁡ card ⁡ 1 … r deg 1 p
73 1 3 2 2 72 cmpo class r ∈ V , j ∈ V ⟼ p ∈ Poly 1 ⁡ r ⟼ rec ⁡ s ∈ V , f ∈ V ⟼ ⦋ mPoly ⁡ s / m⦌ ⦋ g ∈ Monic 1p ⁡ s ∩ Irred ⁡ m | g ∥ r ⁡ m p ∘ f ∧ 1 < s deg 1 g / b⦌ if p ∘ f = 0 m ∨ b = ∅ s f ⦋ glb ⁡ b / h⦌ ⦋ s polyFld h / t⦌ 1 st ⁡ t f ∘ 2 nd ⁡ t j ⁡ card ⁡ 1 … r deg 1 p
74 0 73 wceq wff splitFld 1 = r ∈ V , j ∈ V ⟼ p ∈ Poly 1 ⁡ r ⟼ rec ⁡ s ∈ V , f ∈ V ⟼ ⦋ mPoly ⁡ s / m⦌ ⦋ g ∈ Monic 1p ⁡ s ∩ Irred ⁡ m | g ∥ r ⁡ m p ∘ f ∧ 1 < s deg 1 g / b⦌ if p ∘ f = 0 m ∨ b = ∅ s f ⦋ glb ⁡ b / h⦌ ⦋ s polyFld h / t⦌ 1 st ⁡ t f ∘ 2 nd ⁡ t j ⁡ card ⁡ 1 … r deg 1 p