Definition df-sfl 33503

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 33495	. 2 class splitFld
2		vr	. . 3 setvar 𝑟
3		vp	. . 3 setvar 𝑝
4		cvv 3422	. . 3 class V
5		c1 10803	. . . . . . . 8 class 1
6	3	cv 1538	. . . . . . . . 9 class 𝑝
7		chash 13972	. . . . . . . . 9 class ♯
8	6, 7	cfv 6418	. . . . . . . 8 class (♯‘𝑝)
9		cfz 13168	. . . . . . . 8 class ...
10	5, 8, 9	co 7255	. . . . . . 7 class (1...(♯‘𝑝))
11		clt 10940	. . . . . . 7 class <
12	2	cv 1538	. . . . . . . 8 class 𝑟
13		cplt 17941	. . . . . . . 8 class lt
14	12, 13	cfv 6418	. . . . . . 7 class (lt‘𝑟)
15		vf	. . . . . . . 8 setvar 𝑓
16	15	cv 1538	. . . . . . 7 class 𝑓
17	10, 6, 11, 14, 16	wiso 6419	. . . . . 6 wff 𝑓 Isom < , (lt‘𝑟)((1...(♯‘𝑝)), 𝑝)
18		vx	. . . . . . . 8 setvar 𝑥
19	18	cv 1538	. . . . . . 7 class 𝑥
20		ve	. . . . . . . . . 10 setvar 𝑒
21		vg	. . . . . . . . . 10 setvar 𝑔
22	21	cv 1538	. . . . . . . . . . 11 class 𝑔
23	20	cv 1538	. . . . . . . . . . . 12 class 𝑒
24		csf1 33494	. . . . . . . . . . . 12 class splitFld1
25	12, 23, 24	co 7255	. . . . . . . . . . 11 class (𝑟 splitFld1 𝑒)
26	22, 25	cfv 6418	. . . . . . . . . 10 class ((𝑟 splitFld1 𝑒)‘𝑔)
27	20, 21, 4, 4, 26	cmpo 7257	. . . . . . . . 9 class (𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔))
28		cc0 10802	. . . . . . . . . . . 12 class 0
29		cid 5479	. . . . . . . . . . . . . 14 class I
30		cbs 16840	. . . . . . . . . . . . . . 15 class Base
31	12, 30	cfv 6418	. . . . . . . . . . . . . 14 class (Base‘𝑟)
32	29, 31	cres 5582	. . . . . . . . . . . . 13 class ( I ↾ (Base‘𝑟))
33	12, 32	cop 4564	. . . . . . . . . . . 12 class ⟨𝑟, ( I ↾ (Base‘𝑟))⟩
34	28, 33	cop 4564	. . . . . . . . . . 11 class ⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩
35	34	csn 4558	. . . . . . . . . 10 class {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}
36	16, 35	cun 3881	. . . . . . . . 9 class (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩})
37	27, 36, 28	cseq 13649	. . . . . . . 8 class seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))
38	8, 37	cfv 6418	. . . . . . 7 class (seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))‘(♯‘𝑝))
39	19, 38	wceq 1539	. . . . . 6 wff 𝑥 = (seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))‘(♯‘𝑝))
40	17, 39	wa 395	. . . . 5 wff (𝑓 Isom < , (lt‘𝑟)((1...(♯‘𝑝)), 𝑝) ∧ 𝑥 = (seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))‘(♯‘𝑝)))
41	40, 15	wex 1783	. . . 4 wff ∃𝑓(𝑓 Isom < , (lt‘𝑟)((1...(♯‘𝑝)), 𝑝) ∧ 𝑥 = (seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))‘(♯‘𝑝)))
42	41, 18	cio 6374	. . 3 class (℩𝑥∃𝑓(𝑓 Isom < , (lt‘𝑟)((1...(♯‘𝑝)), 𝑝) ∧ 𝑥 = (seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))‘(♯‘𝑝))))
43	2, 3, 4, 4, 42	cmpo 7257	. 2 class (𝑟 ∈ V, 𝑝 ∈ V ↦ (℩𝑥∃𝑓(𝑓 Isom < , (lt‘𝑟)((1...(♯‘𝑝)), 𝑝) ∧ 𝑥 = (seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))‘(♯‘𝑝)))))
44	1, 43	wceq 1539	1 wff splitFld = (𝑟 ∈ V, 𝑝 ∈ V ↦ (℩𝑥∃𝑓(𝑓 Isom < , (lt‘𝑟)((1...(♯‘𝑝)), 𝑝) ∧ 𝑥 = (seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))‘(♯‘𝑝)))))

This definition is referenced by: (None)