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

Definition df-psr 17351
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 ) ,  (  oF ( +g  `  r )  |`  ( b  X.  b
) ) >. ,  <. ( .r `  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( k  e.  d  |->  ( r  gsumg  ( 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 ) } ) ) >. } ) )
Distinct variable group:    b, d, f, g, h, i, k, r, x, y

Detailed syntax breakdown of Definition df-psr
StepHypRef Expression
1 cmps 17340 . 2  class mPwSer
2 vi . . 3  setvar  i
3 vr . . 3  setvar  r
4 cvv 2962 . . 3  class  _V
5 vd . . . 4  setvar  d
6 vh . . . . . . . . 9  setvar  h
76cv 1361 . . . . . . . 8  class  h
87ccnv 4826 . . . . . . 7  class  `' h
9 cn 10310 . . . . . . 7  class  NN
108, 9cima 4830 . . . . . 6  class  ( `' h " NN )
11 cfn 7298 . . . . . 6  class  Fin
1210, 11wcel 1755 . . . . 5  wff  ( `' h " NN )  e.  Fin
13 cn0 10567 . . . . . 6  class  NN0
142cv 1361 . . . . . 6  class  i
15 cmap 7202 . . . . . 6  class  ^m
1613, 14, 15co 6080 . . . . 5  class  ( NN0 
^m  i )
1712, 6, 16crab 2709 . . . 4  class  { h  e.  ( NN0  ^m  i
)  |  ( `' h " NN )  e.  Fin }
18 vb . . . . 5  setvar  b
193cv 1361 . . . . . . 7  class  r
20 cbs 14157 . . . . . . 7  class  Base
2119, 20cfv 5406 . . . . . 6  class  ( Base `  r )
225cv 1361 . . . . . 6  class  d
2321, 22, 15co 6080 . . . . 5  class  ( (
Base `  r )  ^m  d )
24 cnx 14154 . . . . . . . . 9  class  ndx
2524, 20cfv 5406 . . . . . . . 8  class  ( Base `  ndx )
2618cv 1361 . . . . . . . 8  class  b
2725, 26cop 3871 . . . . . . 7  class  <. ( Base `  ndx ) ,  b >.
28 cplusg 14221 . . . . . . . . 9  class  +g
2924, 28cfv 5406 . . . . . . . 8  class  ( +g  ` 
ndx )
3019, 28cfv 5406 . . . . . . . . . 10  class  ( +g  `  r )
3130cof 6307 . . . . . . . . 9  class  oF ( +g  `  r
)
3226, 26cxp 4825 . . . . . . . . 9  class  ( b  X.  b )
3331, 32cres 4829 . . . . . . . 8  class  (  oF ( +g  `  r
)  |`  ( b  X.  b ) )
3429, 33cop 3871 . . . . . . 7  class  <. ( +g  `  ndx ) ,  (  oF ( +g  `  r )  |`  ( b  X.  b
) ) >.
35 cmulr 14222 . . . . . . . . 9  class  .r
3624, 35cfv 5406 . . . . . . . 8  class  ( .r
`  ndx )
37 vf . . . . . . . . 9  setvar  f
38 vg . . . . . . . . 9  setvar  g
39 vk . . . . . . . . . 10  setvar  k
40 vx . . . . . . . . . . . 12  setvar  x
41 vy . . . . . . . . . . . . . . 15  setvar  y
4241cv 1361 . . . . . . . . . . . . . 14  class  y
4339cv 1361 . . . . . . . . . . . . . 14  class  k
44 cle 9407 . . . . . . . . . . . . . . 15  class  <_
4544cofr 6308 . . . . . . . . . . . . . 14  class  oR  <_
4642, 43, 45wbr 4280 . . . . . . . . . . . . 13  wff  y  oR  <_  k
4746, 41, 22crab 2709 . . . . . . . . . . . 12  class  { y  e.  d  |  y  oR  <_  k }
4840cv 1361 . . . . . . . . . . . . . 14  class  x
4937cv 1361 . . . . . . . . . . . . . 14  class  f
5048, 49cfv 5406 . . . . . . . . . . . . 13  class  ( f `
 x )
51 cmin 9583 . . . . . . . . . . . . . . . 16  class  -
5251cof 6307 . . . . . . . . . . . . . . 15  class  oF  -
5343, 48, 52co 6080 . . . . . . . . . . . . . 14  class  ( k  oF  -  x
)
5438cv 1361 . . . . . . . . . . . . . 14  class  g
5553, 54cfv 5406 . . . . . . . . . . . . 13  class  ( g `
 ( k  oF  -  x ) )
5619, 35cfv 5406 . . . . . . . . . . . . 13  class  ( .r
`  r )
5750, 55, 56co 6080 . . . . . . . . . . . 12  class  ( ( f `  x ) ( .r `  r
) ( g `  ( k  oF  -  x ) ) )
5840, 47, 57cmpt 4338 . . . . . . . . . . 11  class  ( x  e.  { y  e.  d  |  y  oR  <_  k }  |->  ( ( f `  x ) ( .r
`  r ) ( g `  ( k  oF  -  x
) ) ) )
59 cgsu 14362 . . . . . . . . . . 11  class  gsumg
6019, 58, 59co 6080 . . . . . . . . . 10  class  ( r 
gsumg  ( x  e.  { y  e.  d  |  y  oR  <_  k }  |->  ( ( f `
 x ) ( .r `  r ) ( g `  (
k  oF  -  x ) ) ) ) )
6139, 22, 60cmpt 4338 . . . . . . . . 9  class  ( k  e.  d  |->  ( r 
gsumg  ( x  e.  { y  e.  d  |  y  oR  <_  k }  |->  ( ( f `
 x ) ( .r `  r ) ( g `  (
k  oF  -  x ) ) ) ) ) )
6237, 38, 26, 26, 61cmpt2 6082 . . . . . . . 8  class  ( f  e.  b ,  g  e.  b  |->  ( k  e.  d  |->  ( r 
gsumg  ( x  e.  { y  e.  d  |  y  oR  <_  k }  |->  ( ( f `
 x ) ( .r `  r ) ( g `  (
k  oF  -  x ) ) ) ) ) ) )
6336, 62cop 3871 . . . . . . 7  class  <. ( .r `  ndx ) ,  ( f  e.  b ,  g  e.  b 
|->  ( k  e.  d 
|->  ( r  gsumg  ( x  e.  {
y  e.  d  |  y  oR  <_ 
k }  |->  ( ( f `  x ) ( .r `  r
) ( g `  ( k  oF  -  x ) ) ) ) ) ) ) >.
6427, 34, 63ctp 3869 . . . . . 6  class  { <. (
Base `  ndx ) ,  b >. ,  <. ( +g  `  ndx ) ,  (  oF ( +g  `  r )  |`  ( b  X.  b
) ) >. ,  <. ( .r `  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( k  e.  d  |->  ( r  gsumg  ( x  e.  { y  e.  d  |  y  oR  <_  k }  |->  ( ( f `  x ) ( .r
`  r ) ( g `  ( k  oF  -  x
) ) ) ) ) ) ) >. }
65 csca 14224 . . . . . . . . 9  class Scalar
6624, 65cfv 5406 . . . . . . . 8  class  (Scalar `  ndx )
6766, 19cop 3871 . . . . . . 7  class  <. (Scalar ` 
ndx ) ,  r
>.
68 cvsca 14225 . . . . . . . . 9  class  .s
6924, 68cfv 5406 . . . . . . . 8  class  ( .s
`  ndx )
7048csn 3865 . . . . . . . . . . 11  class  { x }
7122, 70cxp 4825 . . . . . . . . . 10  class  ( d  X.  { x }
)
7256cof 6307 . . . . . . . . . 10  class  oF ( .r `  r
)
7371, 49, 72co 6080 . . . . . . . . 9  class  ( ( d  X.  { x } )  oF ( .r `  r
) f )
7440, 37, 21, 26, 73cmpt2 6082 . . . . . . . 8  class  ( x  e.  ( Base `  r
) ,  f  e.  b  |->  ( ( d  X.  { x }
)  oF ( .r `  r ) f ) )
7569, 74cop 3871 . . . . . . 7  class  <. ( .s `  ndx ) ,  ( x  e.  (
Base `  r ) ,  f  e.  b  |->  ( ( d  X. 
{ x } )  oF ( .r
`  r ) f ) ) >.
76 cts 14227 . . . . . . . . 9  class TopSet
7724, 76cfv 5406 . . . . . . . 8  class  (TopSet `  ndx )
78 ctopn 14343 . . . . . . . . . . . 12  class  TopOpen
7919, 78cfv 5406 . . . . . . . . . . 11  class  ( TopOpen `  r )
8079csn 3865 . . . . . . . . . 10  class  { (
TopOpen `  r ) }
8122, 80cxp 4825 . . . . . . . . 9  class  ( d  X.  { ( TopOpen `  r ) } )
82 cpt 14360 . . . . . . . . 9  class  Xt_
8381, 82cfv 5406 . . . . . . . 8  class  ( Xt_ `  ( d  X.  {
( TopOpen `  r ) } ) )
8477, 83cop 3871 . . . . . . 7  class  <. (TopSet ` 
ndx ) ,  (
Xt_ `  ( d  X.  { ( TopOpen `  r
) } ) )
>.
8567, 75, 84ctp 3869 . . . . . 6  class  { <. (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 ) } ) ) >. }
8664, 85cun 3314 . . . . 5  class  ( {
<. ( Base `  ndx ) ,  b >. , 
<. ( +g  `  ndx ) ,  (  oF ( +g  `  r
)  |`  ( b  X.  b ) ) >. ,  <. ( .r `  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( k  e.  d  |->  ( r 
gsumg  ( 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 ) } ) ) >. } )
8718, 23, 86csb 3276 . . . 4  class  [_ (
( 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  gsumg  ( 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 ) } ) ) >. } )
885, 17, 87csb 3276 . . 3  class  [_ {
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  gsumg  ( 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 ) } ) ) >. } )
892, 3, 4, 4, 88cmpt2 6082 . 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 ) ,  (  oF ( +g  `  r )  |`  ( b  X.  b
) ) >. ,  <. ( .r `  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( k  e.  d  |->  ( r  gsumg  ( 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 ) } ) ) >. } ) )
901, 89wceq 1362 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 ) ,  (  oF ( +g  `  r )  |`  ( b  X.  b
) ) >. ,  <. ( .r `  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( k  e.  d  |->  ( r  gsumg  ( 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 ) } ) ) >. } ) )
Colors of variables: wff setvar class
This definition is referenced by:  reldmpsr  17362  psrval  17363
  Copyright terms: Public domain W3C validator