df-psl - Mathbox for Mario Carneiro

	Mathbox for Mario Carneiro		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-psl		Structured version Visualization version Unicode version

Definition df-psl 31537

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

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 splitFld HomLim

Distinct variable group:

**Detailed syntax breakdown of Definition df-psl**
Step	Hyp	Ref	Expression
1		cpsl 31529	. 2 polySplitLim
2		vr	. . 3
3		vp	. . 3
4		cvv 3200	. . 3
5	2	cv 1482	. . . . . . 7
6		cbs 15857	. . . . . . 7
7	5, 6	cfv 5888	. . . . . 6
8	7	cpw 4158	. . . . 5
9		cfn 7955	. . . . 5
10	8, 9	cin 3573	. . . 4
11		cn 11020	. . . 4
12		cmap 7857	. . . 4
13	10, 11, 12	co 6650	. . 3
14		vf	. . . 4
15		c1st 7166	. . . . 5
16		vg	. . . . . . 7
17		vq	. . . . . . 7
18		ve	. . . . . . . 8
19	16	cv 1482	. . . . . . . . 9
20	19, 15	cfv 5888	. . . . . . . 8
21		vs	. . . . . . . . 9
22	18	cv 1482	. . . . . . . . . 10
23	22, 15	cfv 5888	. . . . . . . . 9
24	21	cv 1482	. . . . . . . . . . 11
25		vx	. . . . . . . . . . . . 13
26	17	cv 1482	. . . . . . . . . . . . 13
27	25	cv 1482	. . . . . . . . . . . . . 14
28		c2nd 7167	. . . . . . . . . . . . . . 15
29	19, 28	cfv 5888	. . . . . . . . . . . . . 14
30	27, 29	ccom 5118	. . . . . . . . . . . . 13
31	25, 26, 30	cmpt 4729	. . . . . . . . . . . 12
32	31	crn 5115	. . . . . . . . . . 11
33		csf 31528	. . . . . . . . . . 11 splitFld
34	24, 32, 33	co 6650	. . . . . . . . . 10 splitFld
35	14	cv 1482	. . . . . . . . . . 11
36	35, 28	cfv 5888	. . . . . . . . . . . 12
37	29, 36	ccom 5118	. . . . . . . . . . 11
38	35, 37	cop 4183	. . . . . . . . . 10
39	14, 34, 38	csb 3533	. . . . . . . . 9 splitFld
40	21, 23, 39	csb 3533	. . . . . . . 8 splitFld
41	18, 20, 40	csb 3533	. . . . . . 7 splitFld
42	16, 17, 4, 4, 41	cmpt2 6652	. . . . . 6 splitFld
43	3	cv 1482	. . . . . . 7
44		cc0 9936	. . . . . . . . 9
45		c0 3915	. . . . . . . . . . 11
46	5, 45	cop 4183	. . . . . . . . . 10
47		cid 5023	. . . . . . . . . . 11
48	47, 7	cres 5116	. . . . . . . . . 10
49	46, 48	cop 4183	. . . . . . . . 9
50	44, 49	cop 4183	. . . . . . . 8
51	50	csn 4177	. . . . . . 7
52	43, 51	cun 3572	. . . . . 6
53	42, 52, 44	cseq 12801	. . . . 5 splitFld
54	15, 53	ccom 5118	. . . 4 splitFld
55		c1 9937	. . . . . . 7
56		cshi 13806	. . . . . . 7
57	35, 55, 56	co 6650	. . . . . 6
58	15, 57	ccom 5118	. . . . 5
59	28, 35	ccom 5118	. . . . 5
60		chlim 31525	. . . . 5 HomLim
61	58, 59, 60	co 6650	. . . 4 HomLim
62	14, 54, 61	csb 3533	. . 3 splitFld HomLim
63	2, 3, 4, 13, 62	cmpt2 6652	. 2 splitFld HomLim
64	1, 63	wceq 1483	1 polySplitLim splitFld HomLim

Colors of variables: wff setvar class

This definition is referenced by: (None)

W3C validator