df-sfl

Description: Define the splitting field of a finite collection of polynomials, given a total ordered base field. The output is a tuple <. S , F >. where S is the totally ordered splitting field and F is an injective homomorphism from the original field r . (Contributed by Mario Carneiro, 2-Dec-2014)

		Ref	Expression
	Assertion	df-sfl	$⊢ splitFld = (r \in V, p \in V ⟼ (ι x \| \exists f (f {Isom}_{<, <_{r}} ((1 \dots \|p\|), p) \land x = seq 0 ((e \in V, g \in V ⟼ (r {splitFld}_{1} e) (g)), (f \cup \{⟨0, ⟨r, {I ↾}_{{Base}_{r}}⟩⟩\})) (\|p\|))))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csf	$class splitFld$
1		vr	$setvar r$
2		cvv	$class V$
3		vp	$setvar p$
4		vx	$setvar x$
5		vf	$setvar f$
6	5	cv	$setvar f$
7		clt	$class <$
8		cplt	$class lt$
9	1	cv	$setvar r$
10	9 8	cfv	$class <_{r}$
11		c1	$class 1$
12		cfz	$class \dots$
13		chash	$class \|.\|$
14	3	cv	$setvar p$
15	14 13	cfv	$class \|p\|$
16	11 15 12	co	$class (1 \dots \|p\|)$
17	16 14 7 10 6	wiso	$wff f {Isom}_{<, <_{r}} ((1 \dots \|p\|), p)$
18	4	cv	$setvar x$
19		cc0	$class 0$
20		ve	$setvar e$
21		vg	$setvar g$
22		csf1	$class {splitFld}_{1}$
23	20	cv	$setvar e$
24	9 23 22	co	$class (r {splitFld}_{1} e)$
25	21	cv	$setvar g$
26	25 24	cfv	$class (r {splitFld}_{1} e) (g)$
27	20 21 2 2 26	cmpo	$class (e \in V, g \in V ⟼ (r {splitFld}_{1} e) (g))$
28		cid	$class I$
29		cbs	$class Base$
30	9 29	cfv	$class {Base}_{r}$
31	28 30	cres	$class ({I ↾}_{{Base}_{r}})$
32	9 31	cop	$class ⟨r, {I ↾}_{{Base}_{r}}⟩$
33	19 32	cop	$class ⟨0, ⟨r, {I ↾}_{{Base}_{r}}⟩⟩$
34	33	csn	$class \{⟨0, ⟨r, {I ↾}_{{Base}_{r}}⟩⟩\}$
35	6 34	cun	$class (f \cup \{⟨0, ⟨r, {I ↾}_{{Base}_{r}}⟩⟩\})$
36	27 35 19	cseq	$class seq 0 ((e \in V, g \in V ⟼ (r {splitFld}_{1} e) (g)), (f \cup \{⟨0, ⟨r, {I ↾}_{{Base}_{r}}⟩⟩\}))$
37	15 36	cfv	$class seq 0 ((e \in V, g \in V ⟼ (r {splitFld}_{1} e) (g)), (f \cup \{⟨0, ⟨r, {I ↾}_{{Base}_{r}}⟩⟩\})) (\|p\|)$
38	18 37	wceq	$wff x = seq 0 ((e \in V, g \in V ⟼ (r {splitFld}_{1} e) (g)), (f \cup \{⟨0, ⟨r, {I ↾}_{{Base}_{r}}⟩⟩\})) (\|p\|)$
39	17 38	wa	$wff (f {Isom}_{<, <_{r}} ((1 \dots \|p\|), p) \land x = seq 0 ((e \in V, g \in V ⟼ (r {splitFld}_{1} e) (g)), (f \cup \{⟨0, ⟨r, {I ↾}_{{Base}_{r}}⟩⟩\})) (\|p\|))$
40	39 5	wex	$wff \exists f (f {Isom}_{<, <_{r}} ((1 \dots \|p\|), p) \land x = seq 0 ((e \in V, g \in V ⟼ (r {splitFld}_{1} e) (g)), (f \cup \{⟨0, ⟨r, {I ↾}_{{Base}_{r}}⟩⟩\})) (\|p\|))$
41	40 4	cio	$class (ι x \| \exists f (f {Isom}_{<, <_{r}} ((1 \dots \|p\|), p) \land x = seq 0 ((e \in V, g \in V ⟼ (r {splitFld}_{1} e) (g)), (f \cup \{⟨0, ⟨r, {I ↾}_{{Base}_{r}}⟩⟩\})) (\|p\|)))$
42	1 3 2 2 41	cmpo	$class (r \in V, p \in V ⟼ (ι x \| \exists f (f {Isom}_{<, <_{r}} ((1 \dots \|p\|), p) \land x = seq 0 ((e \in V, g \in V ⟼ (r {splitFld}_{1} e) (g)), (f \cup \{⟨0, ⟨r, {I ↾}_{{Base}_{r}}⟩⟩\})) (\|p\|))))$
43	0 42	wceq	$wff splitFld = (r \in V, p \in V ⟼ (ι x \| \exists f (f {Isom}_{<, <_{r}} ((1 \dots \|p\|), p) \land x = seq 0 ((e \in V, g \in V ⟼ (r {splitFld}_{1} e) (g)), (f \cup \{⟨0, ⟨r, {I ↾}_{{Base}_{r}}⟩⟩\})) (\|p\|))))$

Metamath Proof Explorer

Definition df-sfl

Detailed syntax breakdown