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

Definition df-psl 25069
 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
StepHypRef Expression
1 cpsl 25061 . 2 polySplitLim
2 vr . . 3
3 vp . . 3
4 cvv 2948 . . 3
52cv 1651 . . . . . . 7
6 cbs 13461 . . . . . . 7
75, 6cfv 5446 . . . . . 6
87cpw 3791 . . . . 5
9 cfn 7101 . . . . 5
108, 9cin 3311 . . . 4
11 cn 9992 . . . 4
12 cmap 7010 . . . 4
1310, 11, 12co 6073 . . 3
14 vf . . . 4
15 c1st 6339 . . . . 5
16 vg . . . . . . 7
17 vq . . . . . . 7
18 ve . . . . . . . 8
1916cv 1651 . . . . . . . . 9
2019, 15cfv 5446 . . . . . . . 8
21 vs . . . . . . . . 9
2218cv 1651 . . . . . . . . . 10
2322, 15cfv 5446 . . . . . . . . 9
2421cv 1651 . . . . . . . . . . 11
25 vx . . . . . . . . . . . . 13
2617cv 1651 . . . . . . . . . . . . 13
2725cv 1651 . . . . . . . . . . . . . 14
28 c2nd 6340 . . . . . . . . . . . . . . 15
2919, 28cfv 5446 . . . . . . . . . . . . . 14
3027, 29ccom 4874 . . . . . . . . . . . . 13
3125, 26, 30cmpt 4258 . . . . . . . . . . . 12
3231crn 4871 . . . . . . . . . . 11
33 csf 25060 . . . . . . . . . . 11 splitFld
3424, 32, 33co 6073 . . . . . . . . . 10 splitFld
3514cv 1651 . . . . . . . . . . 11
3635, 28cfv 5446 . . . . . . . . . . . 12
3729, 36ccom 4874 . . . . . . . . . . 11
3835, 37cop 3809 . . . . . . . . . 10
3914, 34, 38csb 3243 . . . . . . . . 9 splitFld
4021, 23, 39csb 3243 . . . . . . . 8 splitFld
4118, 20, 40csb 3243 . . . . . . 7 splitFld
4216, 17, 4, 4, 41cmpt2 6075 . . . . . 6 splitFld
433cv 1651 . . . . . . 7
44 cc0 8982 . . . . . . . . 9
45 c0 3620 . . . . . . . . . . 11
465, 45cop 3809 . . . . . . . . . 10
47 cid 4485 . . . . . . . . . . 11
4847, 7cres 4872 . . . . . . . . . 10
4946, 48cop 3809 . . . . . . . . 9
5044, 49cop 3809 . . . . . . . 8
5150csn 3806 . . . . . . 7
5243, 51cun 3310 . . . . . 6
5342, 52, 44cseq 11315 . . . . 5 splitFld
5415, 53ccom 4874 . . . 4 splitFld
55 c1 8983 . . . . . . 7
56 cshi 11873 . . . . . . 7
5735, 55, 56co 6073 . . . . . 6
5815, 57ccom 4874 . . . . 5
5928, 35ccom 4874 . . . . 5
60 chlim 25057 . . . . 5 HomLim
6158, 59, 60co 6073 . . . 4 HomLim
6214, 54, 61csb 3243 . . 3 splitFld HomLim
632, 3, 4, 13, 62cmpt2 6075 . 2 splitFld HomLim
641, 63wceq 1652 1 polySplitLim splitFld HomLim
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator