MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-psr Unicode version

Definition df-psr 16114
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.)
Assertion
Ref Expression
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 ) ,  (  o F ( +g  `  r )  |`  ( b  X.  b
) ) >. ,  <. ( .r `  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( k  e.  d  |->  ( r  gsumg  ( x  e.  { y  e.  d  |  y  o R  <_  k }  |->  ( ( f `  x ) ( .r
`  r ) ( g `  ( k  o F  -  x
) ) ) ) ) ) ) >. }  u.  { <. (Scalar ` 
ndx ) ,  r
>. ,  <. ( .s
`  ndx ) ,  ( x  e.  ( Base `  r ) ,  f  e.  b  |->  ( ( d  X.  { x } )  o F ( .r `  r
) f ) )
>. ,  <. (TopSet `  ndx ) ,  ( Xt_ `  ( d  X.  {
( TopOpen `  r ) } ) ) >. } ) )
Distinct variable group:    b, d, f, g, h, i, k, r, x, y

Detailed syntax breakdown of Definition df-psr
StepHypRef Expression
1 cmps 16103 . 2  class mPwSer
2 vi . . 3  set  i
3 vr . . 3  set  r
4 cvv 2801 . . 3  class  _V
5 vd . . . 4  set  d
6 vh . . . . . . . . 9  set  h
76cv 1631 . . . . . . . 8  class  h
87ccnv 4704 . . . . . . 7  class  `' h
9 cn 9762 . . . . . . 7  class  NN
108, 9cima 4708 . . . . . 6  class  ( `' h " NN )
11 cfn 6879 . . . . . 6  class  Fin
1210, 11wcel 1696 . . . . 5  wff  ( `' h " NN )  e.  Fin
13 cn0 9981 . . . . . 6  class  NN0
142cv 1631 . . . . . 6  class  i
15 cmap 6788 . . . . . 6  class  ^m
1613, 14, 15co 5874 . . . . 5  class  ( NN0 
^m  i )
1712, 6, 16crab 2560 . . . 4  class  { h  e.  ( NN0  ^m  i
)  |  ( `' h " NN )  e.  Fin }
18 vb . . . . 5  set  b
193cv 1631 . . . . . . 7  class  r
20 cbs 13164 . . . . . . 7  class  Base
2119, 20cfv 5271 . . . . . 6  class  ( Base `  r )
225cv 1631 . . . . . 6  class  d
2321, 22, 15co 5874 . . . . 5  class  ( (
Base `  r )  ^m  d )
24 cnx 13161 . . . . . . . . 9  class  ndx
2524, 20cfv 5271 . . . . . . . 8  class  ( Base `  ndx )
2618cv 1631 . . . . . . . 8  class  b
2725, 26cop 3656 . . . . . . 7  class  <. ( Base `  ndx ) ,  b >.
28 cplusg 13224 . . . . . . . . 9  class  +g
2924, 28cfv 5271 . . . . . . . 8  class  ( +g  ` 
ndx )
3019, 28cfv 5271 . . . . . . . . . 10  class  ( +g  `  r )
3130cof 6092 . . . . . . . . 9  class  o F ( +g  `  r
)
3226, 26cxp 4703 . . . . . . . . 9  class  ( b  X.  b )
3331, 32cres 4707 . . . . . . . 8  class  (  o F ( +g  `  r
)  |`  ( b  X.  b ) )
3429, 33cop 3656 . . . . . . 7  class  <. ( +g  `  ndx ) ,  (  o F ( +g  `  r )  |`  ( b  X.  b
) ) >.
35 cmulr 13225 . . . . . . . . 9  class  .r
3624, 35cfv 5271 . . . . . . . 8  class  ( .r
`  ndx )
37 vf . . . . . . . . 9  set  f
38 vg . . . . . . . . 9  set  g
39 vk . . . . . . . . . 10  set  k
40 vx . . . . . . . . . . . 12  set  x
41 vy . . . . . . . . . . . . . . 15  set  y
4241cv 1631 . . . . . . . . . . . . . 14  class  y
4339cv 1631 . . . . . . . . . . . . . 14  class  k
44 cle 8884 . . . . . . . . . . . . . . 15  class  <_
4544cofr 6093 . . . . . . . . . . . . . 14  class  o R  <_
4642, 43, 45wbr 4039 . . . . . . . . . . . . 13  wff  y  o R  <_  k
4746, 41, 22crab 2560 . . . . . . . . . . . 12  class  { y  e.  d  |  y  o R  <_  k }
4840cv 1631 . . . . . . . . . . . . . 14  class  x
4937cv 1631 . . . . . . . . . . . . . 14  class  f
5048, 49cfv 5271 . . . . . . . . . . . . 13  class  ( f `
 x )
51 cmin 9053 . . . . . . . . . . . . . . . 16  class  -
5251cof 6092 . . . . . . . . . . . . . . 15  class  o F  -
5343, 48, 52co 5874 . . . . . . . . . . . . . 14  class  ( k  o F  -  x
)
5438cv 1631 . . . . . . . . . . . . . 14  class  g
5553, 54cfv 5271 . . . . . . . . . . . . 13  class  ( g `
 ( k  o F  -  x ) )
5619, 35cfv 5271 . . . . . . . . . . . . 13  class  ( .r
`  r )
5750, 55, 56co 5874 . . . . . . . . . . . 12  class  ( ( f `  x ) ( .r `  r
) ( g `  ( k  o F  -  x ) ) )
5840, 47, 57cmpt 4093 . . . . . . . . . . 11  class  ( x  e.  { y  e.  d  |  y  o R  <_  k }  |->  ( ( f `  x ) ( .r
`  r ) ( g `  ( k  o F  -  x
) ) ) )
59 cgsu 13417 . . . . . . . . . . 11  class  gsumg
6019, 58, 59co 5874 . . . . . . . . . 10  class  ( r 
gsumg  ( x  e.  { y  e.  d  |  y  o R  <_  k }  |->  ( ( f `
 x ) ( .r `  r ) ( g `  (
k  o F  -  x ) ) ) ) )
6139, 22, 60cmpt 4093 . . . . . . . . 9  class  ( k  e.  d  |->  ( r 
gsumg  ( x  e.  { y  e.  d  |  y  o R  <_  k }  |->  ( ( f `
 x ) ( .r `  r ) ( g `  (
k  o F  -  x ) ) ) ) ) )
6237, 38, 26, 26, 61cmpt2 5876 . . . . . . . 8  class  ( f  e.  b ,  g  e.  b  |->  ( k  e.  d  |->  ( r 
gsumg  ( x  e.  { y  e.  d  |  y  o R  <_  k }  |->  ( ( f `
 x ) ( .r `  r ) ( g `  (
k  o F  -  x ) ) ) ) ) ) )
6336, 62cop 3656 . . . . . . 7  class  <. ( .r `  ndx ) ,  ( f  e.  b ,  g  e.  b 
|->  ( k  e.  d 
|->  ( r  gsumg  ( x  e.  {
y  e.  d  |  y  o R  <_ 
k }  |->  ( ( f `  x ) ( .r `  r
) ( g `  ( k  o F  -  x ) ) ) ) ) ) ) >.
6427, 34, 63ctp 3655 . . . . . 6  class  { <. (
Base `  ndx ) ,  b >. ,  <. ( +g  `  ndx ) ,  (  o F ( +g  `  r )  |`  ( b  X.  b
) ) >. ,  <. ( .r `  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( k  e.  d  |->  ( r  gsumg  ( x  e.  { y  e.  d  |  y  o R  <_  k }  |->  ( ( f `  x ) ( .r
`  r ) ( g `  ( k  o F  -  x
) ) ) ) ) ) ) >. }
65 csca 13227 . . . . . . . . 9  class Scalar
6624, 65cfv 5271 . . . . . . . 8  class  (Scalar `  ndx )
6766, 19cop 3656 . . . . . . 7  class  <. (Scalar ` 
ndx ) ,  r
>.
68 cvsca 13228 . . . . . . . . 9  class  .s
6924, 68cfv 5271 . . . . . . . 8  class  ( .s
`  ndx )
7048csn 3653 . . . . . . . . . . 11  class  { x }
7122, 70cxp 4703 . . . . . . . . . 10  class  ( d  X.  { x }
)
7256cof 6092 . . . . . . . . . 10  class  o F ( .r `  r
)
7371, 49, 72co 5874 . . . . . . . . 9  class  ( ( d  X.  { x } )  o F ( .r `  r
) f )
7440, 37, 21, 26, 73cmpt2 5876 . . . . . . . 8  class  ( x  e.  ( Base `  r
) ,  f  e.  b  |->  ( ( d  X.  { x }
)  o F ( .r `  r ) f ) )
7569, 74cop 3656 . . . . . . 7  class  <. ( .s `  ndx ) ,  ( x  e.  (
Base `  r ) ,  f  e.  b  |->  ( ( d  X. 
{ x } )  o F ( .r
`  r ) f ) ) >.
76 cts 13230 . . . . . . . . 9  class TopSet
7724, 76cfv 5271 . . . . . . . 8  class  (TopSet `  ndx )
78 ctopn 13342 . . . . . . . . . . . 12  class  TopOpen
7919, 78cfv 5271 . . . . . . . . . . 11  class  ( TopOpen `  r )
8079csn 3653 . . . . . . . . . 10  class  { (
TopOpen `  r ) }
8122, 80cxp 4703 . . . . . . . . 9  class  ( d  X.  { ( TopOpen `  r ) } )
82 cpt 13359 . . . . . . . . 9  class  Xt_
8381, 82cfv 5271 . . . . . . . 8  class  ( Xt_ `  ( d  X.  {
( TopOpen `  r ) } ) )
8477, 83cop 3656 . . . . . . 7  class  <. (TopSet ` 
ndx ) ,  (
Xt_ `  ( d  X.  { ( TopOpen `  r
) } ) )
>.
8567, 75, 84ctp 3655 . . . . . 6  class  { <. (Scalar `  ndx ) ,  r
>. ,  <. ( .s
`  ndx ) ,  ( x  e.  ( Base `  r ) ,  f  e.  b  |->  ( ( d  X.  { x } )  o F ( .r `  r
) f ) )
>. ,  <. (TopSet `  ndx ) ,  ( Xt_ `  ( d  X.  {
( TopOpen `  r ) } ) ) >. }
8664, 85cun 3163 . . . . 5  class  ( {
<. ( Base `  ndx ) ,  b >. , 
<. ( +g  `  ndx ) ,  (  o F ( +g  `  r
)  |`  ( b  X.  b ) ) >. ,  <. ( .r `  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( k  e.  d  |->  ( r 
gsumg  ( x  e.  { y  e.  d  |  y  o R  <_  k }  |->  ( ( f `
 x ) ( .r `  r ) ( g `  (
k  o F  -  x ) ) ) ) ) ) )
>. }  u.  { <. (Scalar `  ndx ) ,  r
>. ,  <. ( .s
`  ndx ) ,  ( x  e.  ( Base `  r ) ,  f  e.  b  |->  ( ( d  X.  { x } )  o F ( .r `  r
) f ) )
>. ,  <. (TopSet `  ndx ) ,  ( Xt_ `  ( d  X.  {
( TopOpen `  r ) } ) ) >. } )
8718, 23, 86csb 3094 . . . 4  class  [_ (
( Base `  r )  ^m  d )  /  b ]_ ( { <. ( Base `  ndx ) ,  b >. ,  <. ( +g  `  ndx ) ,  (  o F ( +g  `  r )  |`  ( b  X.  b
) ) >. ,  <. ( .r `  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( k  e.  d  |->  ( r  gsumg  ( x  e.  { y  e.  d  |  y  o R  <_  k }  |->  ( ( f `  x ) ( .r
`  r ) ( g `  ( k  o F  -  x
) ) ) ) ) ) ) >. }  u.  { <. (Scalar ` 
ndx ) ,  r
>. ,  <. ( .s
`  ndx ) ,  ( x  e.  ( Base `  r ) ,  f  e.  b  |->  ( ( d  X.  { x } )  o F ( .r `  r
) f ) )
>. ,  <. (TopSet `  ndx ) ,  ( Xt_ `  ( d  X.  {
( TopOpen `  r ) } ) ) >. } )
885, 17, 87csb 3094 . . 3  class  [_ {
h  e.  ( NN0 
^m  i )  |  ( `' h " NN )  e.  Fin }  /  d ]_ [_ (
( Base `  r )  ^m  d )  /  b ]_ ( { <. ( Base `  ndx ) ,  b >. ,  <. ( +g  `  ndx ) ,  (  o F ( +g  `  r )  |`  ( b  X.  b
) ) >. ,  <. ( .r `  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( k  e.  d  |->  ( r  gsumg  ( x  e.  { y  e.  d  |  y  o R  <_  k }  |->  ( ( f `  x ) ( .r
`  r ) ( g `  ( k  o F  -  x
) ) ) ) ) ) ) >. }  u.  { <. (Scalar ` 
ndx ) ,  r
>. ,  <. ( .s
`  ndx ) ,  ( x  e.  ( Base `  r ) ,  f  e.  b  |->  ( ( d  X.  { x } )  o F ( .r `  r
) f ) )
>. ,  <. (TopSet `  ndx ) ,  ( Xt_ `  ( d  X.  {
( TopOpen `  r ) } ) ) >. } )
892, 3, 4, 4, 88cmpt2 5876 . 2  class  ( 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 ) ,  (  o F ( +g  `  r )  |`  ( b  X.  b
) ) >. ,  <. ( .r `  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( k  e.  d  |->  ( r  gsumg  ( x  e.  { y  e.  d  |  y  o R  <_  k }  |->  ( ( f `  x ) ( .r
`  r ) ( g `  ( k  o F  -  x
) ) ) ) ) ) ) >. }  u.  { <. (Scalar ` 
ndx ) ,  r
>. ,  <. ( .s
`  ndx ) ,  ( x  e.  ( Base `  r ) ,  f  e.  b  |->  ( ( d  X.  { x } )  o F ( .r `  r
) f ) )
>. ,  <. (TopSet `  ndx ) ,  ( Xt_ `  ( d  X.  {
( TopOpen `  r ) } ) ) >. } ) )
901, 89wceq 1632 1  wff 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 ) ,  (  o F ( +g  `  r )  |`  ( b  X.  b
) ) >. ,  <. ( .r `  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( k  e.  d  |->  ( r  gsumg  ( x  e.  { y  e.  d  |  y  o R  <_  k }  |->  ( ( f `  x ) ( .r
`  r ) ( g `  ( k  o F  -  x
) ) ) ) ) ) ) >. }  u.  { <. (Scalar ` 
ndx ) ,  r
>. ,  <. ( .s
`  ndx ) ,  ( x  e.  ( Base `  r ) ,  f  e.  b  |->  ( ( d  X.  { x } )  o F ( .r `  r
) f ) )
>. ,  <. (TopSet `  ndx ) ,  ( Xt_ `  ( d  X.  {
( TopOpen `  r ) } ) ) >. } ) )
Colors of variables: wff set class
This definition is referenced by:  reldmpsr  16125  psrval  16126
  Copyright terms: Public domain W3C validator