Definition df-sfl 30790

Description: Define the splitting field of a finite collection of polynomials, given a total ordered base field. The output is a tuple ⟨𝑆, 𝐹⟩ where 𝑆 is the totally ordered splitting field and 𝐹 is an injective homomorphism from the original field 𝑟. (Contributed by Mario Carneiro, 2-Dec-2014.)

Assertion

Ref	Expression
df-sfl	⊢ splitFld = (𝑟 ∈ V, 𝑝 ∈ V ↦ (℩𝑥∃𝑓(𝑓 Isom < , (lt‘𝑟)((1...(#‘𝑝)), 𝑝) ∧ 𝑥 = (seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))‘(#‘𝑝)))))

Distinct variable group:   𝑒,𝑓,𝑔,𝑝,𝑟,𝑥

Detailed syntax breakdown of Definition df-sfl

Step	Hyp	Ref	Expression
1		csf 30782	. 2 class splitFld
2		vr	. . 3 setvar 𝑟
3		vp	. . 3 setvar 𝑝
4		cvv 3173	. . 3 class V
5		c1 9816	. . . . . . . 8 class 1
6	3	cv 1474	. . . . . . . . 9 class 𝑝
7		chash 12979	. . . . . . . . 9 class #
8	6, 7	cfv 5804	. . . . . . . 8 class (#‘𝑝)
9		cfz 12197	. . . . . . . 8 class ...
10	5, 8, 9	co 6549	. . . . . . 7 class (1...(#‘𝑝))
11		clt 9953	. . . . . . 7 class <
12	2	cv 1474	. . . . . . . 8 class 𝑟
13		cplt 16764	. . . . . . . 8 class lt
14	12, 13	cfv 5804	. . . . . . 7 class (lt‘𝑟)
15		vf	. . . . . . . 8 setvar 𝑓
16	15	cv 1474	. . . . . . 7 class 𝑓
17	10, 6, 11, 14, 16	wiso 5805	. . . . . 6 wff 𝑓 Isom < , (lt‘𝑟)((1...(#‘𝑝)), 𝑝)
18		vx	. . . . . . . 8 setvar 𝑥
19	18	cv 1474	. . . . . . 7 class 𝑥
20		ve	. . . . . . . . . 10 setvar 𝑒
21		vg	. . . . . . . . . 10 setvar 𝑔
22	21	cv 1474	. . . . . . . . . . 11 class 𝑔
23	20	cv 1474	. . . . . . . . . . . 12 class 𝑒
24		csf1 30781	. . . . . . . . . . . 12 class splitFld1
25	12, 23, 24	co 6549	. . . . . . . . . . 11 class (𝑟 splitFld1 𝑒)
26	22, 25	cfv 5804	. . . . . . . . . 10 class ((𝑟 splitFld1 𝑒)‘𝑔)
27	20, 21, 4, 4, 26	cmpt2 6551	. . . . . . . . 9 class (𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔))
28		cc0 9815	. . . . . . . . . . . 12 class 0
29		cid 4948	. . . . . . . . . . . . . 14 class I
30		cbs 15695	. . . . . . . . . . . . . . 15 class Base
31	12, 30	cfv 5804	. . . . . . . . . . . . . 14 class (Base‘𝑟)
32	29, 31	cres 5040	. . . . . . . . . . . . 13 class ( I ↾ (Base‘𝑟))
33	12, 32	cop 4131	. . . . . . . . . . . 12 class ⟨𝑟, ( I ↾ (Base‘𝑟))⟩
34	28, 33	cop 4131	. . . . . . . . . . 11 class ⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩
35	34	csn 4125	. . . . . . . . . 10 class {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}
36	16, 35	cun 3538	. . . . . . . . 9 class (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩})
37	27, 36, 28	cseq 12663	. . . . . . . 8 class seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))
38	8, 37	cfv 5804	. . . . . . 7 class (seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))‘(#‘𝑝))
39	19, 38	wceq 1475	. . . . . 6 wff 𝑥 = (seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))‘(#‘𝑝))
40	17, 39	wa 383	. . . . 5 wff (𝑓 Isom < , (lt‘𝑟)((1...(#‘𝑝)), 𝑝) ∧ 𝑥 = (seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))‘(#‘𝑝)))
41	40, 15	wex 1695	. . . 4 wff ∃𝑓(𝑓 Isom < , (lt‘𝑟)((1...(#‘𝑝)), 𝑝) ∧ 𝑥 = (seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))‘(#‘𝑝)))
42	41, 18	cio 5766	. . 3 class (℩𝑥∃𝑓(𝑓 Isom < , (lt‘𝑟)((1...(#‘𝑝)), 𝑝) ∧ 𝑥 = (seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))‘(#‘𝑝))))
43	2, 3, 4, 4, 42	cmpt2 6551	. 2 class (𝑟 ∈ V, 𝑝 ∈ V ↦ (℩𝑥∃𝑓(𝑓 Isom < , (lt‘𝑟)((1...(#‘𝑝)), 𝑝) ∧ 𝑥 = (seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))‘(#‘𝑝)))))
44	1, 43	wceq 1475	1 wff splitFld = (𝑟 ∈ V, 𝑝 ∈ V ↦ (℩𝑥∃𝑓(𝑓 Isom < , (lt‘𝑟)((1...(#‘𝑝)), 𝑝) ∧ 𝑥 = (seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))‘(#‘𝑝)))))

This definition is referenced by: (None)