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 \in V, j \in V ⟼ (p \in {Poly}_{1} (r) ⟼ rec ((s \in V, f \in V ⟼ ⦋ mPoly (s) / m ⦌ ⦋ \{g \in ({Monic}_{1p} (s) \cap Irred (m)) \| (g ∥_{r} (m) (p \circ f) \land 1 < s \deg_{1} g)\} / b ⦌ if ((p \circ f = 0_{m} \lor b = \emptyset), ⟨s, f⟩, ⦋ glb (b) / h ⦌ ⦋ (s polyFld h) / t ⦌ ⟨1^{st} (t), f \circ 2^{nd} (t)⟩)), j) (card ((1 \dots 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) \cap 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 \circ f)$
27	21 26 23	wbr	$wff g ∥_{r} (m) (p \circ 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 \circ f) \land 1 < s \deg_{1} g)$
34	33 14 20	crab	$class \{g \in ({Monic}_{1p} (s) \cap Irred (m)) \| (g ∥_{r} (m) (p \circ f) \land 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 \circ f = 0_{m}$
39	35	cv	$setvar b$
40		c0	$class \emptyset$
41	39 40	wceq	$wff b = \emptyset$
42	38 41	wo	$wff (p \circ f = 0_{m} \lor b = \emptyset)$
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 \circ 2^{nd} (t))$
57	53 56	cop	$class ⟨1^{st} (t), f \circ 2^{nd} (t)⟩$
58	50 49 57	csb	$class ⦋ (s polyFld h) / t ⦌ ⟨1^{st} (t), f \circ 2^{nd} (t)⟩$
59	46 45 58	csb	$class ⦋ glb (b) / h ⦌ ⦋ (s polyFld h) / t ⦌ ⟨1^{st} (t), f \circ 2^{nd} (t)⟩$
60	42 43 59	cif	$class if ((p \circ f = 0_{m} \lor b = \emptyset), ⟨s, f⟩, ⦋ glb (b) / h ⦌ ⦋ (s polyFld h) / t ⦌ ⟨1^{st} (t), f \circ 2^{nd} (t)⟩)$
61	35 34 60	csb	$class ⦋ \{g \in ({Monic}_{1p} (s) \cap Irred (m)) \| (g ∥_{r} (m) (p \circ f) \land 1 < s \deg_{1} g)\} / b ⦌ if ((p \circ f = 0_{m} \lor b = \emptyset), ⟨s, f⟩, ⦋ glb (b) / h ⦌ ⦋ (s polyFld h) / t ⦌ ⟨1^{st} (t), f \circ 2^{nd} (t)⟩)$
62	13 12 61	csb	$class ⦋ mPoly (s) / m ⦌ ⦋ \{g \in ({Monic}_{1p} (s) \cap Irred (m)) \| (g ∥_{r} (m) (p \circ f) \land 1 < s \deg_{1} g)\} / b ⦌ if ((p \circ f = 0_{m} \lor b = \emptyset), ⟨s, f⟩, ⦋ glb (b) / h ⦌ ⦋ (s polyFld h) / t ⦌ ⟨1^{st} (t), f \circ 2^{nd} (t)⟩)$
63	8 9 2 2 62	cmpo	$class (s \in V, f \in V ⟼ ⦋ mPoly (s) / m ⦌ ⦋ \{g \in ({Monic}_{1p} (s) \cap Irred (m)) \| (g ∥_{r} (m) (p \circ f) \land 1 < s \deg_{1} g)\} / b ⦌ if ((p \circ f = 0_{m} \lor b = \emptyset), ⟨s, f⟩, ⦋ glb (b) / h ⦌ ⦋ (s polyFld h) / t ⦌ ⟨1^{st} (t), f \circ 2^{nd} (t)⟩))$
64	3	cv	$setvar j$
65	63 64	crdg	$class rec ((s \in V, f \in V ⟼ ⦋ mPoly (s) / m ⦌ ⦋ \{g \in ({Monic}_{1p} (s) \cap Irred (m)) \| (g ∥_{r} (m) (p \circ f) \land 1 < s \deg_{1} g)\} / b ⦌ if ((p \circ f = 0_{m} \lor b = \emptyset), ⟨s, f⟩, ⦋ glb (b) / h ⦌ ⦋ (s polyFld h) / t ⦌ ⟨1^{st} (t), f \circ 2^{nd} (t)⟩)), j)$
66		ccrd	$class card$
67		cfz	$class \dots$
68	6 24 30	co	$class (r \deg_{1} p)$
69	28 68 67	co	$class (1 \dots r \deg_{1} p)$
70	69 66	cfv	$class card ((1 \dots r \deg_{1} p))$
71	70 65	cfv	$class rec ((s \in V, f \in V ⟼ ⦋ mPoly (s) / m ⦌ ⦋ \{g \in ({Monic}_{1p} (s) \cap Irred (m)) \| (g ∥_{r} (m) (p \circ f) \land 1 < s \deg_{1} g)\} / b ⦌ if ((p \circ f = 0_{m} \lor b = \emptyset), ⟨s, f⟩, ⦋ glb (b) / h ⦌ ⦋ (s polyFld h) / t ⦌ ⟨1^{st} (t), f \circ 2^{nd} (t)⟩)), j) (card ((1 \dots r \deg_{1} p)))$
72	4 7 71	cmpt	$class (p \in {Poly}_{1} (r) ⟼ rec ((s \in V, f \in V ⟼ ⦋ mPoly (s) / m ⦌ ⦋ \{g \in ({Monic}_{1p} (s) \cap Irred (m)) \| (g ∥_{r} (m) (p \circ f) \land 1 < s \deg_{1} g)\} / b ⦌ if ((p \circ f = 0_{m} \lor b = \emptyset), ⟨s, f⟩, ⦋ glb (b) / h ⦌ ⦋ (s polyFld h) / t ⦌ ⟨1^{st} (t), f \circ 2^{nd} (t)⟩)), j) (card ((1 \dots r \deg_{1} p))))$
73	1 3 2 2 72	cmpo	$class (r \in V, j \in V ⟼ (p \in {Poly}_{1} (r) ⟼ rec ((s \in V, f \in V ⟼ ⦋ mPoly (s) / m ⦌ ⦋ \{g \in ({Monic}_{1p} (s) \cap Irred (m)) \| (g ∥_{r} (m) (p \circ f) \land 1 < s \deg_{1} g)\} / b ⦌ if ((p \circ f = 0_{m} \lor b = \emptyset), ⟨s, f⟩, ⦋ glb (b) / h ⦌ ⦋ (s polyFld h) / t ⦌ ⟨1^{st} (t), f \circ 2^{nd} (t)⟩)), j) (card ((1 \dots r \deg_{1} p)))))$
74	0 73	wceq	$wff {splitFld}_{1} = (r \in V, j \in V ⟼ (p \in {Poly}_{1} (r) ⟼ rec ((s \in V, f \in V ⟼ ⦋ mPoly (s) / m ⦌ ⦋ \{g \in ({Monic}_{1p} (s) \cap Irred (m)) \| (g ∥_{r} (m) (p \circ f) \land 1 < s \deg_{1} g)\} / b ⦌ if ((p \circ f = 0_{m} \lor b = \emptyset), ⟨s, f⟩, ⦋ glb (b) / h ⦌ ⦋ (s polyFld h) / t ⦌ ⟨1^{st} (t), f \circ 2^{nd} (t)⟩)), j) (card ((1 \dots r \deg_{1} p)))))$

Metamath Proof Explorer

Definition df-sfl1

Detailed syntax breakdown