df-psl

Description: Define the direct limit of an increasing sequence of fields produced by pasting together the splitting fields for each sequence of polynomials. That is, given a ring r , a strict order on r , and a sequence p : NN --> ( ~P r i^i Fin ) of finite sets of polynomials to split, we construct the direct limit system of field extensions by splitting one set at a time and passing the resulting construction to HomLim . (Contributed by Mario Carneiro, 2-Dec-2014)

		Ref	Expression
	Assertion	df-psl	⊢ polySplitLim = ( 𝑟 ∈ V , 𝑝 ∈ ( ( 𝒫 ( Base ‘ 𝑟 ) ∩ Fin ) ↑_m ℕ ) ↦ ⦋ ( 1^st ∘ seq 0 ( ( 𝑔 ∈ V , 𝑞 ∈ V ↦ ⦋ ( 1^st ‘ 𝑔 ) / 𝑒 ⦌ ⦋ ( 1^st ‘ 𝑒 ) / 𝑠 ⦌ ⦋ ( 𝑠 splitFld ran ( 𝑥 ∈ 𝑞 ↦ ( 𝑥 ∘ ( 2^nd ‘ 𝑔 ) ) ) ) / 𝑓 ⦌ ⟨ 𝑓 , ( ( 2^nd ‘ 𝑔 ) ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ ) , ( 𝑝 ∪ { ⟨ 0 , ⟨ ⟨ 𝑟 , ∅ ⟩ , ( I ↾ ( Base ‘ 𝑟 ) ) ⟩ ⟩ } ) ) ) / 𝑓 ⦌ ( ( 1^st ∘ ( 𝑓 shift 1 ) ) HomLim ( 2^nd ∘ 𝑓 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpsl	⊢ polySplitLim
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		vp	⊢ 𝑝
4		cbs	⊢ Base
5	1	cv	⊢ 𝑟
6	5 4	cfv	⊢ ( Base ‘ 𝑟 )
7	6	cpw	⊢ 𝒫 ( Base ‘ 𝑟 )
8		cfn	⊢ Fin
9	7 8	cin	⊢ ( 𝒫 ( Base ‘ 𝑟 ) ∩ Fin )
10		cmap	⊢ ↑_m
11		cn	⊢ ℕ
12	9 11 10	co	⊢ ( ( 𝒫 ( Base ‘ 𝑟 ) ∩ Fin ) ↑_m ℕ )
13		c1st	⊢ 1^st
14		cc0	⊢ 0
15		vg	⊢ 𝑔
16		vq	⊢ 𝑞
17	15	cv	⊢ 𝑔
18	17 13	cfv	⊢ ( 1^st ‘ 𝑔 )
19		ve	⊢ 𝑒
20	19	cv	⊢ 𝑒
21	20 13	cfv	⊢ ( 1^st ‘ 𝑒 )
22		vs	⊢ 𝑠
23	22	cv	⊢ 𝑠
24		csf	⊢ splitFld
25		vx	⊢ 𝑥
26	16	cv	⊢ 𝑞
27	25	cv	⊢ 𝑥
28		c2nd	⊢ 2^nd
29	17 28	cfv	⊢ ( 2^nd ‘ 𝑔 )
30	27 29	ccom	⊢ ( 𝑥 ∘ ( 2^nd ‘ 𝑔 ) )
31	25 26 30	cmpt	⊢ ( 𝑥 ∈ 𝑞 ↦ ( 𝑥 ∘ ( 2^nd ‘ 𝑔 ) ) )
32	31	crn	⊢ ran ( 𝑥 ∈ 𝑞 ↦ ( 𝑥 ∘ ( 2^nd ‘ 𝑔 ) ) )
33	23 32 24	co	⊢ ( 𝑠 splitFld ran ( 𝑥 ∈ 𝑞 ↦ ( 𝑥 ∘ ( 2^nd ‘ 𝑔 ) ) ) )
34		vf	⊢ 𝑓
35	34	cv	⊢ 𝑓
36	35 28	cfv	⊢ ( 2^nd ‘ 𝑓 )
37	29 36	ccom	⊢ ( ( 2^nd ‘ 𝑔 ) ∘ ( 2^nd ‘ 𝑓 ) )
38	35 37	cop	⊢ ⟨ 𝑓 , ( ( 2^nd ‘ 𝑔 ) ∘ ( 2^nd ‘ 𝑓 ) ) ⟩
39	34 33 38	csb	⊢ ⦋ ( 𝑠 splitFld ran ( 𝑥 ∈ 𝑞 ↦ ( 𝑥 ∘ ( 2^nd ‘ 𝑔 ) ) ) ) / 𝑓 ⦌ ⟨ 𝑓 , ( ( 2^nd ‘ 𝑔 ) ∘ ( 2^nd ‘ 𝑓 ) ) ⟩
40	22 21 39	csb	⊢ ⦋ ( 1^st ‘ 𝑒 ) / 𝑠 ⦌ ⦋ ( 𝑠 splitFld ran ( 𝑥 ∈ 𝑞 ↦ ( 𝑥 ∘ ( 2^nd ‘ 𝑔 ) ) ) ) / 𝑓 ⦌ ⟨ 𝑓 , ( ( 2^nd ‘ 𝑔 ) ∘ ( 2^nd ‘ 𝑓 ) ) ⟩
41	19 18 40	csb	⊢ ⦋ ( 1^st ‘ 𝑔 ) / 𝑒 ⦌ ⦋ ( 1^st ‘ 𝑒 ) / 𝑠 ⦌ ⦋ ( 𝑠 splitFld ran ( 𝑥 ∈ 𝑞 ↦ ( 𝑥 ∘ ( 2^nd ‘ 𝑔 ) ) ) ) / 𝑓 ⦌ ⟨ 𝑓 , ( ( 2^nd ‘ 𝑔 ) ∘ ( 2^nd ‘ 𝑓 ) ) ⟩
42	15 16 2 2 41	cmpo	⊢ ( 𝑔 ∈ V , 𝑞 ∈ V ↦ ⦋ ( 1^st ‘ 𝑔 ) / 𝑒 ⦌ ⦋ ( 1^st ‘ 𝑒 ) / 𝑠 ⦌ ⦋ ( 𝑠 splitFld ran ( 𝑥 ∈ 𝑞 ↦ ( 𝑥 ∘ ( 2^nd ‘ 𝑔 ) ) ) ) / 𝑓 ⦌ ⟨ 𝑓 , ( ( 2^nd ‘ 𝑔 ) ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ )
43	3	cv	⊢ 𝑝
44		c0	⊢ ∅
45	5 44	cop	⊢ ⟨ 𝑟 , ∅ ⟩
46		cid	⊢ I
47	46 6	cres	⊢ ( I ↾ ( Base ‘ 𝑟 ) )
48	45 47	cop	⊢ ⟨ ⟨ 𝑟 , ∅ ⟩ , ( I ↾ ( Base ‘ 𝑟 ) ) ⟩
49	14 48	cop	⊢ ⟨ 0 , ⟨ ⟨ 𝑟 , ∅ ⟩ , ( I ↾ ( Base ‘ 𝑟 ) ) ⟩ ⟩
50	49	csn	⊢ { ⟨ 0 , ⟨ ⟨ 𝑟 , ∅ ⟩ , ( I ↾ ( Base ‘ 𝑟 ) ) ⟩ ⟩ }
51	43 50	cun	⊢ ( 𝑝 ∪ { ⟨ 0 , ⟨ ⟨ 𝑟 , ∅ ⟩ , ( I ↾ ( Base ‘ 𝑟 ) ) ⟩ ⟩ } )
52	42 51 14	cseq	⊢ seq 0 ( ( 𝑔 ∈ V , 𝑞 ∈ V ↦ ⦋ ( 1^st ‘ 𝑔 ) / 𝑒 ⦌ ⦋ ( 1^st ‘ 𝑒 ) / 𝑠 ⦌ ⦋ ( 𝑠 splitFld ran ( 𝑥 ∈ 𝑞 ↦ ( 𝑥 ∘ ( 2^nd ‘ 𝑔 ) ) ) ) / 𝑓 ⦌ ⟨ 𝑓 , ( ( 2^nd ‘ 𝑔 ) ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ ) , ( 𝑝 ∪ { ⟨ 0 , ⟨ ⟨ 𝑟 , ∅ ⟩ , ( I ↾ ( Base ‘ 𝑟 ) ) ⟩ ⟩ } ) )
53	13 52	ccom	⊢ ( 1^st ∘ seq 0 ( ( 𝑔 ∈ V , 𝑞 ∈ V ↦ ⦋ ( 1^st ‘ 𝑔 ) / 𝑒 ⦌ ⦋ ( 1^st ‘ 𝑒 ) / 𝑠 ⦌ ⦋ ( 𝑠 splitFld ran ( 𝑥 ∈ 𝑞 ↦ ( 𝑥 ∘ ( 2^nd ‘ 𝑔 ) ) ) ) / 𝑓 ⦌ ⟨ 𝑓 , ( ( 2^nd ‘ 𝑔 ) ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ ) , ( 𝑝 ∪ { ⟨ 0 , ⟨ ⟨ 𝑟 , ∅ ⟩ , ( I ↾ ( Base ‘ 𝑟 ) ) ⟩ ⟩ } ) ) )
54		cshi	⊢ shift
55		c1	⊢ 1
56	35 55 54	co	⊢ ( 𝑓 shift 1 )
57	13 56	ccom	⊢ ( 1^st ∘ ( 𝑓 shift 1 ) )
58		chlim	⊢ HomLim
59	28 35	ccom	⊢ ( 2^nd ∘ 𝑓 )
60	57 59 58	co	⊢ ( ( 1^st ∘ ( 𝑓 shift 1 ) ) HomLim ( 2^nd ∘ 𝑓 ) )
61	34 53 60	csb	⊢ ⦋ ( 1^st ∘ seq 0 ( ( 𝑔 ∈ V , 𝑞 ∈ V ↦ ⦋ ( 1^st ‘ 𝑔 ) / 𝑒 ⦌ ⦋ ( 1^st ‘ 𝑒 ) / 𝑠 ⦌ ⦋ ( 𝑠 splitFld ran ( 𝑥 ∈ 𝑞 ↦ ( 𝑥 ∘ ( 2^nd ‘ 𝑔 ) ) ) ) / 𝑓 ⦌ ⟨ 𝑓 , ( ( 2^nd ‘ 𝑔 ) ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ ) , ( 𝑝 ∪ { ⟨ 0 , ⟨ ⟨ 𝑟 , ∅ ⟩ , ( I ↾ ( Base ‘ 𝑟 ) ) ⟩ ⟩ } ) ) ) / 𝑓 ⦌ ( ( 1^st ∘ ( 𝑓 shift 1 ) ) HomLim ( 2^nd ∘ 𝑓 ) )
62	1 3 2 12 61	cmpo	⊢ ( 𝑟 ∈ V , 𝑝 ∈ ( ( 𝒫 ( Base ‘ 𝑟 ) ∩ Fin ) ↑_m ℕ ) ↦ ⦋ ( 1^st ∘ seq 0 ( ( 𝑔 ∈ V , 𝑞 ∈ V ↦ ⦋ ( 1^st ‘ 𝑔 ) / 𝑒 ⦌ ⦋ ( 1^st ‘ 𝑒 ) / 𝑠 ⦌ ⦋ ( 𝑠 splitFld ran ( 𝑥 ∈ 𝑞 ↦ ( 𝑥 ∘ ( 2^nd ‘ 𝑔 ) ) ) ) / 𝑓 ⦌ ⟨ 𝑓 , ( ( 2^nd ‘ 𝑔 ) ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ ) , ( 𝑝 ∪ { ⟨ 0 , ⟨ ⟨ 𝑟 , ∅ ⟩ , ( I ↾ ( Base ‘ 𝑟 ) ) ⟩ ⟩ } ) ) ) / 𝑓 ⦌ ( ( 1^st ∘ ( 𝑓 shift 1 ) ) HomLim ( 2^nd ∘ 𝑓 ) ) )
63	0 62	wceq	⊢ polySplitLim = ( 𝑟 ∈ V , 𝑝 ∈ ( ( 𝒫 ( Base ‘ 𝑟 ) ∩ Fin ) ↑_m ℕ ) ↦ ⦋ ( 1^st ∘ seq 0 ( ( 𝑔 ∈ V , 𝑞 ∈ V ↦ ⦋ ( 1^st ‘ 𝑔 ) / 𝑒 ⦌ ⦋ ( 1^st ‘ 𝑒 ) / 𝑠 ⦌ ⦋ ( 𝑠 splitFld ran ( 𝑥 ∈ 𝑞 ↦ ( 𝑥 ∘ ( 2^nd ‘ 𝑔 ) ) ) ) / 𝑓 ⦌ ⟨ 𝑓 , ( ( 2^nd ‘ 𝑔 ) ∘ ( 2^nd ‘ 𝑓 ) ) ⟩ ) , ( 𝑝 ∪ { ⟨ 0 , ⟨ ⟨ 𝑟 , ∅ ⟩ , ( I ↾ ( Base ‘ 𝑟 ) ) ⟩ ⟩ } ) ) ) / 𝑓 ⦌ ( ( 1^st ∘ ( 𝑓 shift 1 ) ) HomLim ( 2^nd ∘ 𝑓 ) ) )

Metamath Proof Explorer

Definition df-psl

Detailed syntax breakdown