Metamath Proof Explorer

Definition df-homlim

Description: The input to this function is a sequence (on NN ) of structures R ( n ) and homomorphisms F ( n ) : R ( n ) --> R ( n + 1 ) . The resulting structure is the direct limit of the direct system so defined, and maintains any structures that were present in the original objects. TODO: generalize to directed sets? (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Assertion df-homlim 
|- HomLim = ( r e. _V , f e. _V |-> [_ ( HomLimB ` f ) / e ]_ [_ ( 1st ` e ) / v ]_ [_ ( 2nd ` e ) / g ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. ) >. , <. ( .r ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. ) >. } u. { <. ( TopOpen ` ndx ) , { s e. ~P v | A. n e. NN ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) ) } >. , <. ( dist ` ndx ) , U_ n e. NN ran ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. ) >. , <. ( le ` ndx ) , U_ n e. NN ( `' ( g ` n ) o. ( ( le ` ( r ` n ) ) o. ( g ` n ) ) ) >. } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 chlim 
 |-  HomLim
1 vr 
 |-  r
2 cvv 
 |-  _V
3 vf 
 |-  f
4 chlb 
 |-  HomLimB
5 3 cv 
 |-  f
6 5 4 cfv 
 |-  ( HomLimB ` f )
7 ve 
 |-  e
8 c1st 
 |-  1st
9 7 cv 
 |-  e
10 9 8 cfv 
 |-  ( 1st ` e )
11 vv 
 |-  v
12 c2nd 
 |-  2nd
13 9 12 cfv 
 |-  ( 2nd ` e )
14 vg 
 |-  g
15 cbs 
 |-  Base
16 cnx 
 |-  ndx
17 16 15 cfv 
 |-  ( Base ` ndx )
18 11 cv 
 |-  v
19 17 18 cop 
 |-  <. ( Base ` ndx ) , v >.
20 cplusg 
 |-  +g
21 16 20 cfv 
 |-  ( +g ` ndx )
22 vn 
 |-  n
23 cn 
 |-  NN
24 vx 
 |-  x
25 14 cv 
 |-  g
26 22 cv 
 |-  n
27 26 25 cfv 
 |-  ( g ` n )
28 27 cdm 
 |-  dom ( g ` n )
29 vy 
 |-  y
30 24 cv 
 |-  x
31 30 27 cfv 
 |-  ( ( g ` n ) ` x )
32 29 cv 
 |-  y
33 32 27 cfv 
 |-  ( ( g ` n ) ` y )
34 31 33 cop 
 |-  <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >.
35 1 cv 
 |-  r
36 26 35 cfv 
 |-  ( r ` n )
37 36 20 cfv 
 |-  ( +g ` ( r ` n ) )
38 30 32 37 co 
 |-  ( x ( +g ` ( r ` n ) ) y )
39 38 27 cfv 
 |-  ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) )
40 34 39 cop 
 |-  <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >.
41 24 29 28 28 40 cmpo 
 |-  ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. )
42 41 crn 
 |-  ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. )
43 22 23 42 ciun 
 |-  U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. )
44 21 43 cop 
 |-  <. ( +g ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. ) >.
45 cmulr 
 |-  .r
46 16 45 cfv 
 |-  ( .r ` ndx )
47 36 45 cfv 
 |-  ( .r ` ( r ` n ) )
48 30 32 47 co 
 |-  ( x ( .r ` ( r ` n ) ) y )
49 48 27 cfv 
 |-  ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) )
50 34 49 cop 
 |-  <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >.
51 24 29 28 28 50 cmpo 
 |-  ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. )
52 51 crn 
 |-  ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. )
53 22 23 52 ciun 
 |-  U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. )
54 46 53 cop 
 |-  <. ( .r ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. ) >.
55 19 44 54 ctp 
 |-  { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. ) >. , <. ( .r ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. ) >. }
56 ctopn 
 |-  TopOpen
57 16 56 cfv 
 |-  ( TopOpen ` ndx )
58 vs 
 |-  s
59 18 cpw 
 |-  ~P v
60 27 ccnv 
 |-  `' ( g ` n )
61 58 cv 
 |-  s
62 60 61 cima 
 |-  ( `' ( g ` n ) " s )
63 36 56 cfv 
 |-  ( TopOpen ` ( r ` n ) )
64 62 63 wcel 
 |-  ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) )
65 64 22 23 wral 
 |-  A. n e. NN ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) )
66 65 58 59 crab 
 |-  { s e. ~P v | A. n e. NN ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) ) }
67 57 66 cop 
 |-  <. ( TopOpen ` ndx ) , { s e. ~P v | A. n e. NN ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) ) } >.
68 cds 
 |-  dist
69 16 68 cfv 
 |-  ( dist ` ndx )
70 26 27 cfv 
 |-  ( ( g ` n ) ` n )
71 70 cdm 
 |-  dom ( ( g ` n ) ` n )
72 36 68 cfv 
 |-  ( dist ` ( r ` n ) )
73 30 32 72 co 
 |-  ( x ( dist ` ( r ` n ) ) y )
74 34 73 cop 
 |-  <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >.
75 24 29 71 71 74 cmpo 
 |-  ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. )
76 75 crn 
 |-  ran ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. )
77 22 23 76 ciun 
 |-  U_ n e. NN ran ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. )
78 69 77 cop 
 |-  <. ( dist ` ndx ) , U_ n e. NN ran ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. ) >.
79 cple 
 |-  le
80 16 79 cfv 
 |-  ( le ` ndx )
81 36 79 cfv 
 |-  ( le ` ( r ` n ) )
82 81 27 ccom 
 |-  ( ( le ` ( r ` n ) ) o. ( g ` n ) )
83 60 82 ccom 
 |-  ( `' ( g ` n ) o. ( ( le ` ( r ` n ) ) o. ( g ` n ) ) )
84 22 23 83 ciun 
 |-  U_ n e. NN ( `' ( g ` n ) o. ( ( le ` ( r ` n ) ) o. ( g ` n ) ) )
85 80 84 cop 
 |-  <. ( le ` ndx ) , U_ n e. NN ( `' ( g ` n ) o. ( ( le ` ( r ` n ) ) o. ( g ` n ) ) ) >.
86 67 78 85 ctp 
 |-  { <. ( TopOpen ` ndx ) , { s e. ~P v | A. n e. NN ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) ) } >. , <. ( dist ` ndx ) , U_ n e. NN ran ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. ) >. , <. ( le ` ndx ) , U_ n e. NN ( `' ( g ` n ) o. ( ( le ` ( r ` n ) ) o. ( g ` n ) ) ) >. }
87 55 86 cun 
 |-  ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. ) >. , <. ( .r ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. ) >. } u. { <. ( TopOpen ` ndx ) , { s e. ~P v | A. n e. NN ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) ) } >. , <. ( dist ` ndx ) , U_ n e. NN ran ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. ) >. , <. ( le ` ndx ) , U_ n e. NN ( `' ( g ` n ) o. ( ( le ` ( r ` n ) ) o. ( g ` n ) ) ) >. } )
88 14 13 87 csb 
 |-  [_ ( 2nd ` e ) / g ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. ) >. , <. ( .r ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. ) >. } u. { <. ( TopOpen ` ndx ) , { s e. ~P v | A. n e. NN ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) ) } >. , <. ( dist ` ndx ) , U_ n e. NN ran ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. ) >. , <. ( le ` ndx ) , U_ n e. NN ( `' ( g ` n ) o. ( ( le ` ( r ` n ) ) o. ( g ` n ) ) ) >. } )
89 11 10 88 csb 
 |-  [_ ( 1st ` e ) / v ]_ [_ ( 2nd ` e ) / g ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. ) >. , <. ( .r ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. ) >. } u. { <. ( TopOpen ` ndx ) , { s e. ~P v | A. n e. NN ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) ) } >. , <. ( dist ` ndx ) , U_ n e. NN ran ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. ) >. , <. ( le ` ndx ) , U_ n e. NN ( `' ( g ` n ) o. ( ( le ` ( r ` n ) ) o. ( g ` n ) ) ) >. } )
90 7 6 89 csb 
 |-  [_ ( HomLimB ` f ) / e ]_ [_ ( 1st ` e ) / v ]_ [_ ( 2nd ` e ) / g ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. ) >. , <. ( .r ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. ) >. } u. { <. ( TopOpen ` ndx ) , { s e. ~P v | A. n e. NN ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) ) } >. , <. ( dist ` ndx ) , U_ n e. NN ran ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. ) >. , <. ( le ` ndx ) , U_ n e. NN ( `' ( g ` n ) o. ( ( le ` ( r ` n ) ) o. ( g ` n ) ) ) >. } )
91 1 3 2 2 90 cmpo 
 |-  ( r e. _V , f e. _V |-> [_ ( HomLimB ` f ) / e ]_ [_ ( 1st ` e ) / v ]_ [_ ( 2nd ` e ) / g ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. ) >. , <. ( .r ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. ) >. } u. { <. ( TopOpen ` ndx ) , { s e. ~P v | A. n e. NN ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) ) } >. , <. ( dist ` ndx ) , U_ n e. NN ran ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. ) >. , <. ( le ` ndx ) , U_ n e. NN ( `' ( g ` n ) o. ( ( le ` ( r ` n ) ) o. ( g ` n ) ) ) >. } ) )
92 0 91 wceq 
 |-  HomLim = ( r e. _V , f e. _V |-> [_ ( HomLimB ` f ) / e ]_ [_ ( 1st ` e ) / v ]_ [_ ( 2nd ` e ) / g ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( +g ` ( r ` n ) ) y ) ) >. ) >. , <. ( .r ` ndx ) , U_ n e. NN ran ( x e. dom ( g ` n ) , y e. dom ( g ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( ( g ` n ) ` ( x ( .r ` ( r ` n ) ) y ) ) >. ) >. } u. { <. ( TopOpen ` ndx ) , { s e. ~P v | A. n e. NN ( `' ( g ` n ) " s ) e. ( TopOpen ` ( r ` n ) ) } >. , <. ( dist ` ndx ) , U_ n e. NN ran ( x e. dom ( ( g ` n ) ` n ) , y e. dom ( ( g ` n ) ` n ) |-> <. <. ( ( g ` n ) ` x ) , ( ( g ` n ) ` y ) >. , ( x ( dist ` ( r ` n ) ) y ) >. ) >. , <. ( le ` ndx ) , U_ n e. NN ( `' ( g ` n ) o. ( ( le ` ( r ` n ) ) o. ( g ` n ) ) ) >. } ) )