Metamath Proof Explorer

Definition df-psr

Description: Define the algebra of power series over the index set i and with coefficients from the ring r . (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion df-psr 
|- mPwSer = ( i e. _V , r e. _V |-> [_ { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]_ [_ ( ( Base ` r ) ^m d ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsum ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmps 
 |-  mPwSer
1 vi 
 |-  i
2 cvv 
 |-  _V
3 vr 
 |-  r
4 vh 
 |-  h
5 cn0 
 |-  NN0
6 cmap 
 |-  ^m
7 1 cv 
 |-  i
8 5 7 6 co 
 |-  ( NN0 ^m i )
9 4 cv 
 |-  h
10 9 ccnv 
 |-  `' h
11 cn 
 |-  NN
12 10 11 cima 
 |-  ( `' h " NN )
13 cfn 
 |-  Fin
14 12 13 wcel 
 |-  ( `' h " NN ) e. Fin
15 14 4 8 crab 
 |-  { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin }
16 vd 
 |-  d
17 cbs 
 |-  Base
18 3 cv 
 |-  r
19 18 17 cfv 
 |-  ( Base ` r )
20 16 cv 
 |-  d
21 19 20 6 co 
 |-  ( ( Base ` r ) ^m d )
22 vb 
 |-  b
23 cnx 
 |-  ndx
24 23 17 cfv 
 |-  ( Base ` ndx )
25 22 cv 
 |-  b
26 24 25 cop 
 |-  <. ( Base ` ndx ) , b >.
27 cplusg 
 |-  +g
28 23 27 cfv 
 |-  ( +g ` ndx )
29 18 27 cfv 
 |-  ( +g ` r )
30 29 cof 
 |-  oF ( +g ` r )
31 25 25 cxp 
 |-  ( b X. b )
32 30 31 cres 
 |-  ( oF ( +g ` r ) |` ( b X. b ) )
33 28 32 cop 
 |-  <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >.
34 cmulr 
 |-  .r
35 23 34 cfv 
 |-  ( .r ` ndx )
36 vf 
 |-  f
37 vg 
 |-  g
38 vk 
 |-  k
39 cgsu 
 |-  gsum
40 vx 
 |-  x
41 vy 
 |-  y
42 41 cv 
 |-  y
43 cle 
 |-  <_
44 43 cofr 
 |-  oR <_
45 38 cv 
 |-  k
46 42 45 44 wbr 
 |-  y oR <_ k
47 46 41 20 crab 
 |-  { y e. d | y oR <_ k }
48 36 cv 
 |-  f
49 40 cv 
 |-  x
50 49 48 cfv 
 |-  ( f ` x )
51 18 34 cfv 
 |-  ( .r ` r )
52 37 cv 
 |-  g
53 cmin 
 |-  -
54 53 cof 
 |-  oF -
55 45 49 54 co 
 |-  ( k oF - x )
56 55 52 cfv 
 |-  ( g ` ( k oF - x ) )
57 50 56 51 co 
 |-  ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) )
58 40 47 57 cmpt 
 |-  ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) )
59 18 58 39 co 
 |-  ( r gsum ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) )
60 38 20 59 cmpt 
 |-  ( k e. d |-> ( r gsum ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) )
61 36 37 25 25 60 cmpo 
 |-  ( f e. b , g e. b |-> ( k e. d |-> ( r gsum ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) )
62 35 61 cop 
 |-  <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsum ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >.
63 26 33 62 ctp 
 |-  { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsum ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. }
64 csca 
 |-  Scalar
65 23 64 cfv 
 |-  ( Scalar ` ndx )
66 65 18 cop 
 |-  <. ( Scalar ` ndx ) , r >.
67 cvsca 
 |-  .s
68 23 67 cfv 
 |-  ( .s ` ndx )
69 49 csn 
 |-  { x }
70 20 69 cxp 
 |-  ( d X. { x } )
71 51 cof 
 |-  oF ( .r ` r )
72 70 48 71 co 
 |-  ( ( d X. { x } ) oF ( .r ` r ) f )
73 40 36 19 25 72 cmpo 
 |-  ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) )
74 68 73 cop 
 |-  <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >.
75 cts 
 |-  TopSet
76 23 75 cfv 
 |-  ( TopSet ` ndx )
77 cpt 
 |-  Xt_
78 ctopn 
 |-  TopOpen
79 18 78 cfv 
 |-  ( TopOpen ` r )
80 79 csn 
 |-  { ( TopOpen ` r ) }
81 20 80 cxp 
 |-  ( d X. { ( TopOpen ` r ) } )
82 81 77 cfv 
 |-  ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) )
83 76 82 cop 
 |-  <. ( TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >.
84 66 74 83 ctp 
 |-  { <. ( Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. }
85 63 84 cun 
 |-  ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsum ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } )
86 22 21 85 csb 
 |-  [_ ( ( Base ` r ) ^m d ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsum ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } )
87 16 15 86 csb 
 |-  [_ { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]_ [_ ( ( Base ` r ) ^m d ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsum ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } )
88 1 3 2 2 87 cmpo 
 |-  ( i e. _V , r e. _V |-> [_ { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]_ [_ ( ( Base ` r ) ^m d ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsum ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } ) )
89 0 88 wceq 
 |-  mPwSer = ( i e. _V , r e. _V |-> [_ { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]_ [_ ( ( Base ` r ) ^m d ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsum ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } ) )