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