Definition df-psl 36380

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 𝑟, a strict order on 𝑟, and a sequence 𝑝:ℕ⟶(𝒫 𝑟 ∩ 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.)

Assertion

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

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

Detailed syntax breakdown of Definition df-psl

Step	Hyp	Ref	Expression
1		cpsl 36367	. 2 class polySplitLim
2		vr	. . 3 setvar 𝑟
3		vp	. . 3 setvar 𝑝
4		cvv 3451	. . 3 class V
5	2	cv 1569	. . . . . . 7 class 𝑟
6		cbs 17367	. . . . . . 7 class Base
7	5, 6	cfv 6531	. . . . . 6 class (Base‘𝑟)
8	7	cpw 4557	. . . . 5 class 𝒫 (Base‘𝑟)
9		cfn 8957	. . . . 5 class Fin
10	8, 9	cin 3898	. . . 4 class (𝒫 (Base‘𝑟) ∩ Fin)
11		cn 12316	. . . 4 class ℕ
12		cmap 8831	. . . 4 class ↑m
13	10, 11, 12	co 7412	. . 3 class ((𝒫 (Base‘𝑟) ∩ Fin) ↑m ℕ)
14		vf	. . . 4 setvar 𝑓
15		c1st 7988	. . . . 5 class 1st
16		vg	. . . . . . 7 setvar 𝑔
17		vq	. . . . . . 7 setvar 𝑞
18		ve	. . . . . . . 8 setvar 𝑒
19	16	cv 1569	. . . . . . . . 9 class 𝑔
20	19, 15	cfv 6531	. . . . . . . 8 class (1st ‘𝑔)
21		vs	. . . . . . . . 9 setvar 𝑠
22	18	cv 1569	. . . . . . . . . 10 class 𝑒
23	22, 15	cfv 6531	. . . . . . . . 9 class (1st ‘𝑒)
24	21	cv 1569	. . . . . . . . . . 11 class 𝑠
25		vx	. . . . . . . . . . . . 13 setvar 𝑥
26	17	cv 1569	. . . . . . . . . . . . 13 class 𝑞
27	25	cv 1569	. . . . . . . . . . . . . 14 class 𝑥
28		c2nd 7989	. . . . . . . . . . . . . . 15 class 2nd
29	19, 28	cfv 6531	. . . . . . . . . . . . . 14 class (2nd ‘𝑔)
30	27, 29	ccom 5655	. . . . . . . . . . . . 13 class (𝑥 ∘ (2nd ‘𝑔))
31	25, 26, 30	cmpt 5186	. . . . . . . . . . . 12 class (𝑥 ∈ 𝑞 ↦ (𝑥 ∘ (2nd ‘𝑔)))
32	31	crn 5652	. . . . . . . . . . 11 class ran (𝑥 ∈ 𝑞 ↦ (𝑥 ∘ (2nd ‘𝑔)))
33		csf 36366	. . . . . . . . . . 11 class splitFld
34	24, 32, 33	co 7412	. . . . . . . . . 10 class (𝑠 splitFld ran (𝑥 ∈ 𝑞 ↦ (𝑥 ∘ (2nd ‘𝑔))))
35	14	cv 1569	. . . . . . . . . . 11 class 𝑓
36	35, 28	cfv 6531	. . . . . . . . . . . 12 class (2nd ‘𝑓)
37	29, 36	ccom 5655	. . . . . . . . . . 11 class ((2nd ‘𝑔) ∘ (2nd ‘𝑓))
38	35, 37	cop 4590	. . . . . . . . . 10 class ⟨𝑓, ((2nd ‘𝑔) ∘ (2nd ‘𝑓))⟩
39	14, 34, 38	csb 3847	. . . . . . . . 9 class ⦋(𝑠 splitFld ran (𝑥 ∈ 𝑞 ↦ (𝑥 ∘ (2nd ‘𝑔)))) / 𝑓⦌⟨𝑓, ((2nd ‘𝑔) ∘ (2nd ‘𝑓))⟩
40	21, 23, 39	csb 3847	. . . . . . . 8 class ⦋(1st ‘𝑒) / 𝑠⦌⦋(𝑠 splitFld ran (𝑥 ∈ 𝑞 ↦ (𝑥 ∘ (2nd ‘𝑔)))) / 𝑓⦌⟨𝑓, ((2nd ‘𝑔) ∘ (2nd ‘𝑓))⟩
41	18, 20, 40	csb 3847	. . . . . . 7 class ⦋(1st ‘𝑔) / 𝑒⦌⦋(1st ‘𝑒) / 𝑠⦌⦋(𝑠 splitFld ran (𝑥 ∈ 𝑞 ↦ (𝑥 ∘ (2nd ‘𝑔)))) / 𝑓⦌⟨𝑓, ((2nd ‘𝑔) ∘ (2nd ‘𝑓))⟩
42	16, 17, 4, 4, 41	cmpo 7414	. . . . . 6 class (𝑔 ∈ V, 𝑞 ∈ V ↦ ⦋(1st ‘𝑔) / 𝑒⦌⦋(1st ‘𝑒) / 𝑠⦌⦋(𝑠 splitFld ran (𝑥 ∈ 𝑞 ↦ (𝑥 ∘ (2nd ‘𝑔)))) / 𝑓⦌⟨𝑓, ((2nd ‘𝑔) ∘ (2nd ‘𝑓))⟩)
43	3	cv 1569	. . . . . . 7 class 𝑝
44		cc0 11181	. . . . . . . . 9 class 0
45		c0 4279	. . . . . . . . . . 11 class ∅
46	5, 45	cop 4590	. . . . . . . . . 10 class ⟨𝑟, ∅⟩
47		cid 5545	. . . . . . . . . . 11 class I
48	47, 7	cres 5653	. . . . . . . . . 10 class ( I ↾ (Base‘𝑟))
49	46, 48	cop 4590	. . . . . . . . 9 class ⟨⟨𝑟, ∅⟩, ( I ↾ (Base‘𝑟))⟩
50	44, 49	cop 4590	. . . . . . . 8 class ⟨0, ⟨⟨𝑟, ∅⟩, ( I ↾ (Base‘𝑟))⟩⟩
51	50	csn 4584	. . . . . . 7 class {⟨0, ⟨⟨𝑟, ∅⟩, ( I ↾ (Base‘𝑟))⟩⟩}
52	43, 51	cun 3897	. . . . . 6 class (𝑝 ∪ {⟨0, ⟨⟨𝑟, ∅⟩, ( I ↾ (Base‘𝑟))⟩⟩})
53	42, 52, 44	cseq 14124	. . . . 5 class seq0((𝑔 ∈ V, 𝑞 ∈ V ↦ ⦋(1st ‘𝑔) / 𝑒⦌⦋(1st ‘𝑒) / 𝑠⦌⦋(𝑠 splitFld ran (𝑥 ∈ 𝑞 ↦ (𝑥 ∘ (2nd ‘𝑔)))) / 𝑓⦌⟨𝑓, ((2nd ‘𝑔) ∘ (2nd ‘𝑓))⟩), (𝑝 ∪ {⟨0, ⟨⟨𝑟, ∅⟩, ( I ↾ (Base‘𝑟))⟩⟩}))
54	15, 53	ccom 5655	. . . 4 class (1st ∘ seq0((𝑔 ∈ V, 𝑞 ∈ V ↦ ⦋(1st ‘𝑔) / 𝑒⦌⦋(1st ‘𝑒) / 𝑠⦌⦋(𝑠 splitFld ran (𝑥 ∈ 𝑞 ↦ (𝑥 ∘ (2nd ‘𝑔)))) / 𝑓⦌⟨𝑓, ((2nd ‘𝑔) ∘ (2nd ‘𝑓))⟩), (𝑝 ∪ {⟨0, ⟨⟨𝑟, ∅⟩, ( I ↾ (Base‘𝑟))⟩⟩})))
55		c1 11182	. . . . . . 7 class 1
56		cshi 15199	. . . . . . 7 class shift
57	35, 55, 56	co 7412	. . . . . 6 class (𝑓 shift 1)
58	15, 57	ccom 5655	. . . . 5 class (1st ∘ (𝑓 shift 1))
59	28, 35	ccom 5655	. . . . 5 class (2nd ∘ 𝑓)
60		chlim 36363	. . . . 5 class HomLim
61	58, 59, 60	co 7412	. . . 4 class ((1st ∘ (𝑓 shift 1)) HomLim (2nd ∘ 𝑓))
62	14, 54, 61	csb 3847	. . 3 class ⦋(1st ∘ seq0((𝑔 ∈ V, 𝑞 ∈ V ↦ ⦋(1st ‘𝑔) / 𝑒⦌⦋(1st ‘𝑒) / 𝑠⦌⦋(𝑠 splitFld ran (𝑥 ∈ 𝑞 ↦ (𝑥 ∘ (2nd ‘𝑔)))) / 𝑓⦌⟨𝑓, ((2nd ‘𝑔) ∘ (2nd ‘𝑓))⟩), (𝑝 ∪ {⟨0, ⟨⟨𝑟, ∅⟩, ( I ↾ (Base‘𝑟))⟩⟩}))) / 𝑓⦌((1st ∘ (𝑓 shift 1)) HomLim (2nd ∘ 𝑓))
63	2, 3, 4, 13, 62	cmpo 7414	. 2 class (𝑟 ∈ V, 𝑝 ∈ ((𝒫 (Base‘𝑟) ∩ Fin) ↑m ℕ) ↦ ⦋(1st ∘ seq0((𝑔 ∈ V, 𝑞 ∈ V ↦ ⦋(1st ‘𝑔) / 𝑒⦌⦋(1st ‘𝑒) / 𝑠⦌⦋(𝑠 splitFld ran (𝑥 ∈ 𝑞 ↦ (𝑥 ∘ (2nd ‘𝑔)))) / 𝑓⦌⟨𝑓, ((2nd ‘𝑔) ∘ (2nd ‘𝑓))⟩), (𝑝 ∪ {⟨0, ⟨⟨𝑟, ∅⟩, ( I ↾ (Base‘𝑟))⟩⟩}))) / 𝑓⦌((1st ∘ (𝑓 shift 1)) HomLim (2nd ∘ 𝑓)))
64	1, 63	wceq 1570	1 wff polySplitLim = (𝑟 ∈ V, 𝑝 ∈ ((𝒫 (Base‘𝑟) ∩ Fin) ↑m ℕ) ↦ ⦋(1st ∘ seq0((𝑔 ∈ V, 𝑞 ∈ V ↦ ⦋(1st ‘𝑔) / 𝑒⦌⦋(1st ‘𝑒) / 𝑠⦌⦋(𝑠 splitFld ran (𝑥 ∈ 𝑞 ↦ (𝑥 ∘ (2nd ‘𝑔)))) / 𝑓⦌⟨𝑓, ((2nd ‘𝑔) ∘ (2nd ‘𝑓))⟩), (𝑝 ∪ {⟨0, ⟨⟨𝑟, ∅⟩, ( I ↾ (Base‘𝑟))⟩⟩}))) / 𝑓⦌((1st ∘ (𝑓 shift 1)) HomLim (2nd ∘ 𝑓)))

This definition is used by: (None)