Definition 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	$$⊢\mathrm{polySplitLim}=\left(r\in \mathrm{V},p\in \left({\left(𝒫{\mathrm{Base}}_r\cap \mathrm{Fin}\right)}^{\mathbb{N}}\right)⟼⦋\left(1^{st}\circ seq0\left(\left(g\in \mathrm{V},q\in \mathrm{V}⟼⦋1^{st}\left(g\right)/e⦌⦋1^{st}\left(e\right)/s⦌⦋\left(s\mathrm{splitFld}\mathrm{ran}\left(x\in q⟼x\circ 2^{nd}\left(g\right)\right)\right)/f⦌⟨f,2^{nd}\left(g\right)\circ 2^{nd}\left(f\right)⟩\right),\left(p\cup \left\{⟨0,⟨⟨r,\varnothing ⟩,{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_r}⟩⟩\right\}\right)\right)\right)/f⦌\left(\left(1^{st}\circ \left(f\mathrm{shift}1\right)\right)\mathrm{HomLim}\left(2^{nd}\circ f\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpsl	$$class\mathrm{polySplitLim}$$
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		vp	$$setvarp$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarr$$
6	5 4	cfv	$$class{\mathrm{Base}}_r$$
7	6	cpw	$$class𝒫{\mathrm{Base}}_r$$
8		cfn	$$class\mathrm{Fin}$$
9	7 8	cin	$$class\left(𝒫{\mathrm{Base}}_r\cap \mathrm{Fin}\right)$$
10		cmap	$$class{\uparrow }_{𝑚}$$
11		cn	$$class\mathbb{N}$$
12	9 11 10	co	$$class\left({\left(𝒫{\mathrm{Base}}_r\cap \mathrm{Fin}\right)}^{\mathbb{N}}\right)$$
13		c1st	$$class{1}^{st}$$
14		cc0	$$class0$$
15		vg	$$setvarg$$
16		vq	$$setvarq$$
17	15	cv	$$setvarg$$
18	17 13	cfv	$$class{1}^{st}\left(g\right)$$
19		ve	$$setvare$$
20	19	cv	$$setvare$$
21	20 13	cfv	$$class{1}^{st}\left(e\right)$$
22		vs	$$setvars$$
23	22	cv	$$setvars$$
24		csf	$$class\mathrm{splitFld}$$
25		vx	$$setvarx$$
26	16	cv	$$setvarq$$
27	25	cv	$$setvarx$$
28		c2nd	$$class{2}^{nd}$$
29	17 28	cfv	$$class{2}^{nd}\left(g\right)$$
30	27 29	ccom	$$class\left(x\circ 2^{nd}\left(g\right)\right)$$
31	25 26 30	cmpt	$$class\left(x\in q⟼x\circ 2^{nd}\left(g\right)\right)$$
32	31	crn	$$class\mathrm{ran}\left(x\in q⟼x\circ 2^{nd}\left(g\right)\right)$$
33	23 32 24	co	$$class\left(s\mathrm{splitFld}\mathrm{ran}\left(x\in q⟼x\circ 2^{nd}\left(g\right)\right)\right)$$
34		vf	$$setvarf$$
35	34	cv	$$setvarf$$
36	35 28	cfv	$$class{2}^{nd}\left(f\right)$$
37	29 36	ccom	$$class\left(2^{nd}\left(g\right)\circ 2^{nd}\left(f\right)\right)$$
38	35 37	cop	$$class⟨f,2^{nd}\left(g\right)\circ 2^{nd}\left(f\right)⟩$$
39	34 33 38	csb	$$class⦋\left(s\mathrm{splitFld}\mathrm{ran}\left(x\in q⟼x\circ 2^{nd}\left(g\right)\right)\right)/f⦌⟨f,2^{nd}\left(g\right)\circ 2^{nd}\left(f\right)⟩$$
40	22 21 39	csb	$$class⦋1^{st}\left(e\right)/s⦌⦋\left(s\mathrm{splitFld}\mathrm{ran}\left(x\in q⟼x\circ 2^{nd}\left(g\right)\right)\right)/f⦌⟨f,2^{nd}\left(g\right)\circ 2^{nd}\left(f\right)⟩$$
41	19 18 40	csb	$$class⦋1^{st}\left(g\right)/e⦌⦋1^{st}\left(e\right)/s⦌⦋\left(s\mathrm{splitFld}\mathrm{ran}\left(x\in q⟼x\circ 2^{nd}\left(g\right)\right)\right)/f⦌⟨f,2^{nd}\left(g\right)\circ 2^{nd}\left(f\right)⟩$$
42	15 16 2 2 41	cmpo	$$class\left(g\in \mathrm{V},q\in \mathrm{V}⟼⦋1^{st}\left(g\right)/e⦌⦋1^{st}\left(e\right)/s⦌⦋\left(s\mathrm{splitFld}\mathrm{ran}\left(x\in q⟼x\circ 2^{nd}\left(g\right)\right)\right)/f⦌⟨f,2^{nd}\left(g\right)\circ 2^{nd}\left(f\right)⟩\right)$$
43	3	cv	$$setvarp$$
44		c0	$$class\varnothing$$
45	5 44	cop	$$class⟨r,\varnothing ⟩$$
46		cid	$$class\mathrm{I}$$
47	46 6	cres	$$class\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_r}\right)$$
48	45 47	cop	$$class⟨⟨r,\varnothing ⟩,{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_r}⟩$$
49	14 48	cop	$$class⟨0,⟨⟨r,\varnothing ⟩,{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_r}⟩⟩$$
50	49	csn	$$class\left\{⟨0,⟨⟨r,\varnothing ⟩,{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_r}⟩⟩\right\}$$
51	43 50	cun	$$class\left(p\cup \left\{⟨0,⟨⟨r,\varnothing ⟩,{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_r}⟩⟩\right\}\right)$$
52	42 51 14	cseq	$$classseq0\left(\left(g\in \mathrm{V},q\in \mathrm{V}⟼⦋1^{st}\left(g\right)/e⦌⦋1^{st}\left(e\right)/s⦌⦋\left(s\mathrm{splitFld}\mathrm{ran}\left(x\in q⟼x\circ 2^{nd}\left(g\right)\right)\right)/f⦌⟨f,2^{nd}\left(g\right)\circ 2^{nd}\left(f\right)⟩\right),\left(p\cup \left\{⟨0,⟨⟨r,\varnothing ⟩,{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_r}⟩⟩\right\}\right)\right)$$
53	13 52	ccom	$$class\left(1^{st}\circ seq0\left(\left(g\in \mathrm{V},q\in \mathrm{V}⟼⦋1^{st}\left(g\right)/e⦌⦋1^{st}\left(e\right)/s⦌⦋\left(s\mathrm{splitFld}\mathrm{ran}\left(x\in q⟼x\circ 2^{nd}\left(g\right)\right)\right)/f⦌⟨f,2^{nd}\left(g\right)\circ 2^{nd}\left(f\right)⟩\right),\left(p\cup \left\{⟨0,⟨⟨r,\varnothing ⟩,{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_r}⟩⟩\right\}\right)\right)\right)$$
54		cshi	$$class\mathrm{shift}$$
55		c1	$$class1$$
56	35 55 54	co	$$class\left(f\mathrm{shift}1\right)$$
57	13 56	ccom	$$class\left(1^{st}\circ \left(f\mathrm{shift}1\right)\right)$$
58		chlim	$$class\mathrm{HomLim}$$
59	28 35	ccom	$$class\left(2^{nd}\circ f\right)$$
60	57 59 58	co	$$class\left(\left(1^{st}\circ \left(f\mathrm{shift}1\right)\right)\mathrm{HomLim}\left(2^{nd}\circ f\right)\right)$$
61	34 53 60	csb	$$class⦋\left(1^{st}\circ seq0\left(\left(g\in \mathrm{V},q\in \mathrm{V}⟼⦋1^{st}\left(g\right)/e⦌⦋1^{st}\left(e\right)/s⦌⦋\left(s\mathrm{splitFld}\mathrm{ran}\left(x\in q⟼x\circ 2^{nd}\left(g\right)\right)\right)/f⦌⟨f,2^{nd}\left(g\right)\circ 2^{nd}\left(f\right)⟩\right),\left(p\cup \left\{⟨0,⟨⟨r,\varnothing ⟩,{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_r}⟩⟩\right\}\right)\right)\right)/f⦌\left(\left(1^{st}\circ \left(f\mathrm{shift}1\right)\right)\mathrm{HomLim}\left(2^{nd}\circ f\right)\right)$$
62	1 3 2 12 61	cmpo	$$class\left(r\in \mathrm{V},p\in \left({\left(𝒫{\mathrm{Base}}_r\cap \mathrm{Fin}\right)}^{\mathbb{N}}\right)⟼⦋\left(1^{st}\circ seq0\left(\left(g\in \mathrm{V},q\in \mathrm{V}⟼⦋1^{st}\left(g\right)/e⦌⦋1^{st}\left(e\right)/s⦌⦋\left(s\mathrm{splitFld}\mathrm{ran}\left(x\in q⟼x\circ 2^{nd}\left(g\right)\right)\right)/f⦌⟨f,2^{nd}\left(g\right)\circ 2^{nd}\left(f\right)⟩\right),\left(p\cup \left\{⟨0,⟨⟨r,\varnothing ⟩,{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_r}⟩⟩\right\}\right)\right)\right)/f⦌\left(\left(1^{st}\circ \left(f\mathrm{shift}1\right)\right)\mathrm{HomLim}\left(2^{nd}\circ f\right)\right)\right)$$
63	0 62	wceq	$$wff\mathrm{polySplitLim}=\left(r\in \mathrm{V},p\in \left({\left(𝒫{\mathrm{Base}}_r\cap \mathrm{Fin}\right)}^{\mathbb{N}}\right)⟼⦋\left(1^{st}\circ seq0\left(\left(g\in \mathrm{V},q\in \mathrm{V}⟼⦋1^{st}\left(g\right)/e⦌⦋1^{st}\left(e\right)/s⦌⦋\left(s\mathrm{splitFld}\mathrm{ran}\left(x\in q⟼x\circ 2^{nd}\left(g\right)\right)\right)/f⦌⟨f,2^{nd}\left(g\right)\circ 2^{nd}\left(f\right)⟩\right),\left(p\cup \left\{⟨0,⟨⟨r,\varnothing ⟩,{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_r}⟩⟩\right\}\right)\right)\right)/f⦌\left(\left(1^{st}\circ \left(f\mathrm{shift}1\right)\right)\mathrm{HomLim}\left(2^{nd}\circ f\right)\right)\right)$$