Definition df-sfl 34661

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 34654	. 2 class splitFld
2		vr	. . 3 setvar 𝑟
3		vp	. . 3 setvar 𝑝
4		cvv 3475	. . 3 class V
5		c1 11111	. . . . . . . 8 class 1
6	3	cv 1541	. . . . . . . . 9 class 𝑝
7		chash 14290	. . . . . . . . 9 class ♯
8	6, 7	cfv 6544	. . . . . . . 8 class (♯‘𝑝)
9		cfz 13484	. . . . . . . 8 class ...
10	5, 8, 9	co 7409	. . . . . . 7 class (1...(♯‘𝑝))
11		clt 11248	. . . . . . 7 class <
12	2	cv 1541	. . . . . . . 8 class 𝑟
13		cplt 18261	. . . . . . . 8 class lt
14	12, 13	cfv 6544	. . . . . . 7 class (lt‘𝑟)
15		vf	. . . . . . . 8 setvar 𝑓
16	15	cv 1541	. . . . . . 7 class 𝑓
17	10, 6, 11, 14, 16	wiso 6545	. . . . . 6 wff 𝑓 Isom < , (lt‘𝑟)((1...(♯‘𝑝)), 𝑝)
18		vx	. . . . . . . 8 setvar 𝑥
19	18	cv 1541	. . . . . . 7 class 𝑥
20		ve	. . . . . . . . . 10 setvar 𝑒
21		vg	. . . . . . . . . 10 setvar 𝑔
22	21	cv 1541	. . . . . . . . . . 11 class 𝑔
23	20	cv 1541	. . . . . . . . . . . 12 class 𝑒
24		csf1 34653	. . . . . . . . . . . 12 class splitFld1
25	12, 23, 24	co 7409	. . . . . . . . . . 11 class (𝑟 splitFld1 𝑒)
26	22, 25	cfv 6544	. . . . . . . . . 10 class ((𝑟 splitFld1 𝑒)‘𝑔)
27	20, 21, 4, 4, 26	cmpo 7411	. . . . . . . . 9 class (𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔))
28		cc0 11110	. . . . . . . . . . . 12 class 0
29		cid 5574	. . . . . . . . . . . . . 14 class I
30		cbs 17144	. . . . . . . . . . . . . . 15 class Base
31	12, 30	cfv 6544	. . . . . . . . . . . . . 14 class (Base‘𝑟)
32	29, 31	cres 5679	. . . . . . . . . . . . 13 class ( I ↾ (Base‘𝑟))
33	12, 32	cop 4635	. . . . . . . . . . . 12 class ⟨𝑟, ( I ↾ (Base‘𝑟))⟩
34	28, 33	cop 4635	. . . . . . . . . . 11 class ⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩
35	34	csn 4629	. . . . . . . . . 10 class {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}
36	16, 35	cun 3947	. . . . . . . . 9 class (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩})
37	27, 36, 28	cseq 13966	. . . . . . . 8 class seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))
38	8, 37	cfv 6544	. . . . . . 7 class (seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))‘(♯‘𝑝))
39	19, 38	wceq 1542	. . . . . 6 wff 𝑥 = (seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))‘(♯‘𝑝))
40	17, 39	wa 397	. . . . 5 wff (𝑓 Isom < , (lt‘𝑟)((1...(♯‘𝑝)), 𝑝) ∧ 𝑥 = (seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))‘(♯‘𝑝)))
41	40, 15	wex 1782	. . . 4 wff ∃𝑓(𝑓 Isom < , (lt‘𝑟)((1...(♯‘𝑝)), 𝑝) ∧ 𝑥 = (seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))‘(♯‘𝑝)))
42	41, 18	cio 6494	. . 3 class (℩𝑥∃𝑓(𝑓 Isom < , (lt‘𝑟)((1...(♯‘𝑝)), 𝑝) ∧ 𝑥 = (seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))‘(♯‘𝑝))))
43	2, 3, 4, 4, 42	cmpo 7411	. 2 class (𝑟 ∈ V, 𝑝 ∈ V ↦ (℩𝑥∃𝑓(𝑓 Isom < , (lt‘𝑟)((1...(♯‘𝑝)), 𝑝) ∧ 𝑥 = (seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))‘(♯‘𝑝)))))
44	1, 43	wceq 1542	1 wff splitFld = (𝑟 ∈ V, 𝑝 ∈ V ↦ (℩𝑥∃𝑓(𝑓 Isom < , (lt‘𝑟)((1...(♯‘𝑝)), 𝑝) ∧ 𝑥 = (seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))‘(♯‘𝑝)))))

This definition is referenced by: (None)