Metamath Proof Explorer

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 
|- polySplitLim = ( r e. _V , p e. ( ( ~P ( Base ` r ) i^i Fin ) ^m NN ) |-> [_ ( 1st o. seq 0 ( ( g e. _V , q e. _V |-> [_ ( 1st ` g ) / e ]_ [_ ( 1st ` e ) / s ]_ [_ ( s splitFld ran ( x e. q |-> ( x o. ( 2nd ` g ) ) ) ) / f ]_ <. f , ( ( 2nd ` g ) o. ( 2nd ` f ) ) >. ) , ( p u. { <. 0 , <. <. r , (/) >. , ( _I |` ( Base ` r ) ) >. >. } ) ) ) / f ]_ ( ( 1st o. ( f shift 1 ) ) HomLim ( 2nd o. f ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpsl 
 |-  polySplitLim
1 vr 
 |-  r
2 cvv 
 |-  _V
3 vp 
 |-  p
4 cbs 
 |-  Base
5 1 cv 
 |-  r
6 5 4 cfv 
 |-  ( Base ` r )
7 6 cpw 
 |-  ~P ( Base ` r )
8 cfn 
 |-  Fin
9 7 8 cin 
 |-  ( ~P ( Base ` r ) i^i Fin )
10 cmap 
 |-  ^m
11 cn 
 |-  NN
12 9 11 10 co 
 |-  ( ( ~P ( Base ` r ) i^i Fin ) ^m NN )
13 c1st 
 |-  1st
14 cc0 
 |-  0
15 vg 
 |-  g
16 vq 
 |-  q
17 15 cv 
 |-  g
18 17 13 cfv 
 |-  ( 1st ` g )
19 ve 
 |-  e
20 19 cv 
 |-  e
21 20 13 cfv 
 |-  ( 1st ` e )
22 vs 
 |-  s
23 22 cv 
 |-  s
24 csf 
 |-  splitFld
25 vx 
 |-  x
26 16 cv 
 |-  q
27 25 cv 
 |-  x
28 c2nd 
 |-  2nd
29 17 28 cfv 
 |-  ( 2nd ` g )
30 27 29 ccom 
 |-  ( x o. ( 2nd ` g ) )
31 25 26 30 cmpt 
 |-  ( x e. q |-> ( x o. ( 2nd ` g ) ) )
32 31 crn 
 |-  ran ( x e. q |-> ( x o. ( 2nd ` g ) ) )
33 23 32 24 co 
 |-  ( s splitFld ran ( x e. q |-> ( x o. ( 2nd ` g ) ) ) )
34 vf 
 |-  f
35 34 cv 
 |-  f
36 35 28 cfv 
 |-  ( 2nd ` f )
37 29 36 ccom 
 |-  ( ( 2nd ` g ) o. ( 2nd ` f ) )
38 35 37 cop 
 |-  <. f , ( ( 2nd ` g ) o. ( 2nd ` f ) ) >.
39 34 33 38 csb 
 |-  [_ ( s splitFld ran ( x e. q |-> ( x o. ( 2nd ` g ) ) ) ) / f ]_ <. f , ( ( 2nd ` g ) o. ( 2nd ` f ) ) >.
40 22 21 39 csb 
 |-  [_ ( 1st ` e ) / s ]_ [_ ( s splitFld ran ( x e. q |-> ( x o. ( 2nd ` g ) ) ) ) / f ]_ <. f , ( ( 2nd ` g ) o. ( 2nd ` f ) ) >.
41 19 18 40 csb 
 |-  [_ ( 1st ` g ) / e ]_ [_ ( 1st ` e ) / s ]_ [_ ( s splitFld ran ( x e. q |-> ( x o. ( 2nd ` g ) ) ) ) / f ]_ <. f , ( ( 2nd ` g ) o. ( 2nd ` f ) ) >.
42 15 16 2 2 41 cmpo 
 |-  ( g e. _V , q e. _V |-> [_ ( 1st ` g ) / e ]_ [_ ( 1st ` e ) / s ]_ [_ ( s splitFld ran ( x e. q |-> ( x o. ( 2nd ` g ) ) ) ) / f ]_ <. f , ( ( 2nd ` g ) o. ( 2nd ` f ) ) >. )
43 3 cv 
 |-  p
44 c0 
 |-  (/)
45 5 44 cop 
 |-  <. r , (/) >.
46 cid 
 |-  _I
47 46 6 cres 
 |-  ( _I |` ( Base ` r ) )
48 45 47 cop 
 |-  <. <. r , (/) >. , ( _I |` ( Base ` r ) ) >.
49 14 48 cop 
 |-  <. 0 , <. <. r , (/) >. , ( _I |` ( Base ` r ) ) >. >.
50 49 csn 
 |-  { <. 0 , <. <. r , (/) >. , ( _I |` ( Base ` r ) ) >. >. }
51 43 50 cun 
 |-  ( p u. { <. 0 , <. <. r , (/) >. , ( _I |` ( Base ` r ) ) >. >. } )
52 42 51 14 cseq 
 |-  seq 0 ( ( g e. _V , q e. _V |-> [_ ( 1st ` g ) / e ]_ [_ ( 1st ` e ) / s ]_ [_ ( s splitFld ran ( x e. q |-> ( x o. ( 2nd ` g ) ) ) ) / f ]_ <. f , ( ( 2nd ` g ) o. ( 2nd ` f ) ) >. ) , ( p u. { <. 0 , <. <. r , (/) >. , ( _I |` ( Base ` r ) ) >. >. } ) )
53 13 52 ccom 
 |-  ( 1st o. seq 0 ( ( g e. _V , q e. _V |-> [_ ( 1st ` g ) / e ]_ [_ ( 1st ` e ) / s ]_ [_ ( s splitFld ran ( x e. q |-> ( x o. ( 2nd ` g ) ) ) ) / f ]_ <. f , ( ( 2nd ` g ) o. ( 2nd ` f ) ) >. ) , ( p u. { <. 0 , <. <. r , (/) >. , ( _I |` ( Base ` r ) ) >. >. } ) ) )
54 cshi 
 |-  shift
55 c1 
 |-  1
56 35 55 54 co 
 |-  ( f shift 1 )
57 13 56 ccom 
 |-  ( 1st o. ( f shift 1 ) )
58 chlim 
 |-  HomLim
59 28 35 ccom 
 |-  ( 2nd o. f )
60 57 59 58 co 
 |-  ( ( 1st o. ( f shift 1 ) ) HomLim ( 2nd o. f ) )
61 34 53 60 csb 
 |-  [_ ( 1st o. seq 0 ( ( g e. _V , q e. _V |-> [_ ( 1st ` g ) / e ]_ [_ ( 1st ` e ) / s ]_ [_ ( s splitFld ran ( x e. q |-> ( x o. ( 2nd ` g ) ) ) ) / f ]_ <. f , ( ( 2nd ` g ) o. ( 2nd ` f ) ) >. ) , ( p u. { <. 0 , <. <. r , (/) >. , ( _I |` ( Base ` r ) ) >. >. } ) ) ) / f ]_ ( ( 1st o. ( f shift 1 ) ) HomLim ( 2nd o. f ) )
62 1 3 2 12 61 cmpo 
 |-  ( r e. _V , p e. ( ( ~P ( Base ` r ) i^i Fin ) ^m NN ) |-> [_ ( 1st o. seq 0 ( ( g e. _V , q e. _V |-> [_ ( 1st ` g ) / e ]_ [_ ( 1st ` e ) / s ]_ [_ ( s splitFld ran ( x e. q |-> ( x o. ( 2nd ` g ) ) ) ) / f ]_ <. f , ( ( 2nd ` g ) o. ( 2nd ` f ) ) >. ) , ( p u. { <. 0 , <. <. r , (/) >. , ( _I |` ( Base ` r ) ) >. >. } ) ) ) / f ]_ ( ( 1st o. ( f shift 1 ) ) HomLim ( 2nd o. f ) ) )
63 0 62 wceq 
 |-  polySplitLim = ( r e. _V , p e. ( ( ~P ( Base ` r ) i^i Fin ) ^m NN ) |-> [_ ( 1st o. seq 0 ( ( g e. _V , q e. _V |-> [_ ( 1st ` g ) / e ]_ [_ ( 1st ` e ) / s ]_ [_ ( s splitFld ran ( x e. q |-> ( x o. ( 2nd ` g ) ) ) ) / f ]_ <. f , ( ( 2nd ` g ) o. ( 2nd ` f ) ) >. ) , ( p u. { <. 0 , <. <. r , (/) >. , ( _I |` ( Base ` r ) ) >. >. } ) ) ) / f ]_ ( ( 1st o. ( f shift 1 ) ) HomLim ( 2nd o. f ) ) )