Metamath Proof Explorer

Definition 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 ∈ V , p ∈ V ⟼ ι x | ∃ f f Isom < , < r 1 … p p ∧ x = seq 0 e ∈ V , g ∈ V ⟼ r splitFld 1 e ⁡ g f ∪ 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 …
13 chash class .
14 3 cv setvar p
15 14 13 cfv class p
16 11 15 12 co class 1 … p
17 16 14 7 10 6 wiso wff f Isom < , < r 1 … 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 ∈ V , g ∈ 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 ∪ 0 r I ↾ Base r
36 27 35 19 cseq class seq 0 e ∈ V , g ∈ V ⟼ r splitFld 1 e ⁡ g f ∪ 0 r I ↾ Base r
37 15 36 cfv class seq 0 e ∈ V , g ∈ V ⟼ r splitFld 1 e ⁡ g f ∪ 0 r I ↾ Base r ⁡ p
38 18 37 wceq wff x = seq 0 e ∈ V , g ∈ V ⟼ r splitFld 1 e ⁡ g f ∪ 0 r I ↾ Base r ⁡ p
39 17 38 wa wff f Isom < , < r 1 … p p ∧ x = seq 0 e ∈ V , g ∈ V ⟼ r splitFld 1 e ⁡ g f ∪ 0 r I ↾ Base r ⁡ p
40 39 5 wex wff ∃ f f Isom < , < r 1 … p p ∧ x = seq 0 e ∈ V , g ∈ V ⟼ r splitFld 1 e ⁡ g f ∪ 0 r I ↾ Base r ⁡ p
41 40 4 cio class ι x | ∃ f f Isom < , < r 1 … p p ∧ x = seq 0 e ∈ V , g ∈ V ⟼ r splitFld 1 e ⁡ g f ∪ 0 r I ↾ Base r ⁡ p
42 1 3 2 2 41 cmpo class r ∈ V , p ∈ V ⟼ ι x | ∃ f f Isom < , < r 1 … p p ∧ x = seq 0 e ∈ V , g ∈ V ⟼ r splitFld 1 e ⁡ g f ∪ 0 r I ↾ Base r ⁡ p
43 0 42 wceq wff splitFld = r ∈ V , p ∈ V ⟼ ι x | ∃ f f Isom < , < r 1 … p p ∧ x = seq 0 e ∈ V , g ∈ V ⟼ r splitFld 1 e ⁡ g f ∪ 0 r I ↾ Base r ⁡ p