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 = ( 𝑟 ∈ V , 𝑝 ∈ V ↦ ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 Isom < , ( lt ‘ 𝑟 ) ( ( 1 ... ( ♯ ‘ 𝑝 ) ) , 𝑝 ) ∧ 𝑥 = ( seq 0 ( ( 𝑒 ∈ V , 𝑔 ∈ V ↦ ( ( 𝑟 splitFld1 𝑒 ) ‘ 𝑔 ) ) , ( 𝑓 ∪ { ⟨ 0 , ⟨ 𝑟 , ( I ↾ ( Base ‘ 𝑟 ) ) ⟩ ⟩ } ) ) ‘ ( ♯ ‘ 𝑝 ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csf	⊢ splitFld
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		vp	⊢ 𝑝
4		vx	⊢ 𝑥
5		vf	⊢ 𝑓
6	5	cv	⊢ 𝑓
7		clt	⊢ <
8		cplt	⊢ lt
9	1	cv	⊢ 𝑟
10	9 8	cfv	⊢ ( lt ‘ 𝑟 )
11		c1	⊢ 1
12		cfz	⊢ ...
13		chash	⊢ ♯
14	3	cv	⊢ 𝑝
15	14 13	cfv	⊢ ( ♯ ‘ 𝑝 )
16	11 15 12	co	⊢ ( 1 ... ( ♯ ‘ 𝑝 ) )
17	16 14 7 10 6	wiso	⊢ 𝑓 Isom < , ( lt ‘ 𝑟 ) ( ( 1 ... ( ♯ ‘ 𝑝 ) ) , 𝑝 )
18	4	cv	⊢ 𝑥
19		cc0	⊢ 0
20		ve	⊢ 𝑒
21		vg	⊢ 𝑔
22		csf1	⊢ splitFld1
23	20	cv	⊢ 𝑒
24	9 23 22	co	⊢ ( 𝑟 splitFld1 𝑒 )
25	21	cv	⊢ 𝑔
26	25 24	cfv	⊢ ( ( 𝑟 splitFld1 𝑒 ) ‘ 𝑔 )
27	20 21 2 2 26	cmpo	⊢ ( 𝑒 ∈ V , 𝑔 ∈ V ↦ ( ( 𝑟 splitFld1 𝑒 ) ‘ 𝑔 ) )
28		cid	⊢ I
29		cbs	⊢ Base
30	9 29	cfv	⊢ ( Base ‘ 𝑟 )
31	28 30	cres	⊢ ( I ↾ ( Base ‘ 𝑟 ) )
32	9 31	cop	⊢ ⟨ 𝑟 , ( I ↾ ( Base ‘ 𝑟 ) ) ⟩
33	19 32	cop	⊢ ⟨ 0 , ⟨ 𝑟 , ( I ↾ ( Base ‘ 𝑟 ) ) ⟩ ⟩
34	33	csn	⊢ { ⟨ 0 , ⟨ 𝑟 , ( I ↾ ( Base ‘ 𝑟 ) ) ⟩ ⟩ }
35	6 34	cun	⊢ ( 𝑓 ∪ { ⟨ 0 , ⟨ 𝑟 , ( I ↾ ( Base ‘ 𝑟 ) ) ⟩ ⟩ } )
36	27 35 19	cseq	⊢ seq 0 ( ( 𝑒 ∈ V , 𝑔 ∈ V ↦ ( ( 𝑟 splitFld1 𝑒 ) ‘ 𝑔 ) ) , ( 𝑓 ∪ { ⟨ 0 , ⟨ 𝑟 , ( I ↾ ( Base ‘ 𝑟 ) ) ⟩ ⟩ } ) )
37	15 36	cfv	⊢ ( seq 0 ( ( 𝑒 ∈ V , 𝑔 ∈ V ↦ ( ( 𝑟 splitFld1 𝑒 ) ‘ 𝑔 ) ) , ( 𝑓 ∪ { ⟨ 0 , ⟨ 𝑟 , ( I ↾ ( Base ‘ 𝑟 ) ) ⟩ ⟩ } ) ) ‘ ( ♯ ‘ 𝑝 ) )
38	18 37	wceq	⊢ 𝑥 = ( seq 0 ( ( 𝑒 ∈ V , 𝑔 ∈ V ↦ ( ( 𝑟 splitFld1 𝑒 ) ‘ 𝑔 ) ) , ( 𝑓 ∪ { ⟨ 0 , ⟨ 𝑟 , ( I ↾ ( Base ‘ 𝑟 ) ) ⟩ ⟩ } ) ) ‘ ( ♯ ‘ 𝑝 ) )
39	17 38	wa	⊢ ( 𝑓 Isom < , ( lt ‘ 𝑟 ) ( ( 1 ... ( ♯ ‘ 𝑝 ) ) , 𝑝 ) ∧ 𝑥 = ( seq 0 ( ( 𝑒 ∈ V , 𝑔 ∈ V ↦ ( ( 𝑟 splitFld1 𝑒 ) ‘ 𝑔 ) ) , ( 𝑓 ∪ { ⟨ 0 , ⟨ 𝑟 , ( I ↾ ( Base ‘ 𝑟 ) ) ⟩ ⟩ } ) ) ‘ ( ♯ ‘ 𝑝 ) ) )
40	39 5	wex	⊢ ∃ 𝑓 ( 𝑓 Isom < , ( lt ‘ 𝑟 ) ( ( 1 ... ( ♯ ‘ 𝑝 ) ) , 𝑝 ) ∧ 𝑥 = ( seq 0 ( ( 𝑒 ∈ V , 𝑔 ∈ V ↦ ( ( 𝑟 splitFld1 𝑒 ) ‘ 𝑔 ) ) , ( 𝑓 ∪ { ⟨ 0 , ⟨ 𝑟 , ( I ↾ ( Base ‘ 𝑟 ) ) ⟩ ⟩ } ) ) ‘ ( ♯ ‘ 𝑝 ) ) )
41	40 4	cio	⊢ ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 Isom < , ( lt ‘ 𝑟 ) ( ( 1 ... ( ♯ ‘ 𝑝 ) ) , 𝑝 ) ∧ 𝑥 = ( seq 0 ( ( 𝑒 ∈ V , 𝑔 ∈ V ↦ ( ( 𝑟 splitFld1 𝑒 ) ‘ 𝑔 ) ) , ( 𝑓 ∪ { ⟨ 0 , ⟨ 𝑟 , ( I ↾ ( Base ‘ 𝑟 ) ) ⟩ ⟩ } ) ) ‘ ( ♯ ‘ 𝑝 ) ) ) )
42	1 3 2 2 41	cmpo	⊢ ( 𝑟 ∈ V , 𝑝 ∈ V ↦ ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 Isom < , ( lt ‘ 𝑟 ) ( ( 1 ... ( ♯ ‘ 𝑝 ) ) , 𝑝 ) ∧ 𝑥 = ( seq 0 ( ( 𝑒 ∈ V , 𝑔 ∈ V ↦ ( ( 𝑟 splitFld1 𝑒 ) ‘ 𝑔 ) ) , ( 𝑓 ∪ { ⟨ 0 , ⟨ 𝑟 , ( I ↾ ( Base ‘ 𝑟 ) ) ⟩ ⟩ } ) ) ‘ ( ♯ ‘ 𝑝 ) ) ) ) )
43	0 42	wceq	⊢ splitFld = ( 𝑟 ∈ V , 𝑝 ∈ V ↦ ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 Isom < , ( lt ‘ 𝑟 ) ( ( 1 ... ( ♯ ‘ 𝑝 ) ) , 𝑝 ) ∧ 𝑥 = ( seq 0 ( ( 𝑒 ∈ V , 𝑔 ∈ V ↦ ( ( 𝑟 splitFld1 𝑒 ) ‘ 𝑔 ) ) , ( 𝑓 ∪ { ⟨ 0 , ⟨ 𝑟 , ( I ↾ ( Base ‘ 𝑟 ) ) ⟩ ⟩ } ) ) ‘ ( ♯ ‘ 𝑝 ) ) ) ) )