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

Definition df-mvr 17404
Description: Define the generating elements of the power series algebra. (Contributed by Mario Carneiro, 7-Jan-2015.)
Assertion
Ref Expression
df-mvr  |- mVar  =  ( i  e.  _V , 
r  e.  _V  |->  ( x  e.  i  |->  ( f  e.  { h  e.  ( NN0  ^m  i
)  |  ( `' h " NN )  e.  Fin }  |->  if ( f  =  ( y  e.  i  |->  if ( y  =  x ,  1 ,  0 ) ) ,  ( 1r `  r ) ,  ( 0g `  r ) ) ) ) )
Distinct variable group:    f, h, i, r, x, y

Detailed syntax breakdown of Definition df-mvr
StepHypRef Expression
1 cmvr 17399 . 2  class mVar
2 vi . . 3  setvar  i
3 vr . . 3  setvar  r
4 cvv 2967 . . 3  class  _V
5 vx . . . 4  setvar  x
62cv 1368 . . . 4  class  i
7 vf . . . . 5  setvar  f
8 vh . . . . . . . . . 10  setvar  h
98cv 1368 . . . . . . . . 9  class  h
109ccnv 4834 . . . . . . . 8  class  `' h
11 cn 10314 . . . . . . . 8  class  NN
1210, 11cima 4838 . . . . . . 7  class  ( `' h " NN )
13 cfn 7302 . . . . . . 7  class  Fin
1412, 13wcel 1756 . . . . . 6  wff  ( `' h " NN )  e.  Fin
15 cn0 10571 . . . . . . 7  class  NN0
16 cmap 7206 . . . . . . 7  class  ^m
1715, 6, 16co 6086 . . . . . 6  class  ( NN0 
^m  i )
1814, 8, 17crab 2714 . . . . 5  class  { h  e.  ( NN0  ^m  i
)  |  ( `' h " NN )  e.  Fin }
197cv 1368 . . . . . . 7  class  f
20 vy . . . . . . . 8  setvar  y
2120, 5weq 1695 . . . . . . . . 9  wff  y  =  x
22 c1 9275 . . . . . . . . 9  class  1
23 cc0 9274 . . . . . . . . 9  class  0
2421, 22, 23cif 3786 . . . . . . . 8  class  if ( y  =  x ,  1 ,  0 )
2520, 6, 24cmpt 4345 . . . . . . 7  class  ( y  e.  i  |->  if ( y  =  x ,  1 ,  0 ) )
2619, 25wceq 1369 . . . . . 6  wff  f  =  ( y  e.  i 
|->  if ( y  =  x ,  1 ,  0 ) )
273cv 1368 . . . . . . 7  class  r
28 cur 16593 . . . . . . 7  class  1r
2927, 28cfv 5413 . . . . . 6  class  ( 1r
`  r )
30 c0g 14370 . . . . . . 7  class  0g
3127, 30cfv 5413 . . . . . 6  class  ( 0g
`  r )
3226, 29, 31cif 3786 . . . . 5  class  if ( f  =  ( y  e.  i  |->  if ( y  =  x ,  1 ,  0 ) ) ,  ( 1r
`  r ) ,  ( 0g `  r
) )
337, 18, 32cmpt 4345 . . . 4  class  ( f  e.  { h  e.  ( NN0  ^m  i
)  |  ( `' h " NN )  e.  Fin }  |->  if ( f  =  ( y  e.  i  |->  if ( y  =  x ,  1 ,  0 ) ) ,  ( 1r `  r ) ,  ( 0g `  r ) ) )
345, 6, 33cmpt 4345 . . 3  class  ( x  e.  i  |->  ( f  e.  { h  e.  ( NN0  ^m  i
)  |  ( `' h " NN )  e.  Fin }  |->  if ( f  =  ( y  e.  i  |->  if ( y  =  x ,  1 ,  0 ) ) ,  ( 1r `  r ) ,  ( 0g `  r ) ) ) )
352, 3, 4, 4, 34cmpt2 6088 . 2  class  ( i  e.  _V ,  r  e.  _V  |->  ( x  e.  i  |->  ( f  e.  { h  e.  ( NN0  ^m  i
)  |  ( `' h " NN )  e.  Fin }  |->  if ( f  =  ( y  e.  i  |->  if ( y  =  x ,  1 ,  0 ) ) ,  ( 1r `  r ) ,  ( 0g `  r ) ) ) ) )
361, 35wceq 1369 1  wff mVar  =  ( i  e.  _V , 
r  e.  _V  |->  ( x  e.  i  |->  ( f  e.  { h  e.  ( NN0  ^m  i
)  |  ( `' h " NN )  e.  Fin }  |->  if ( f  =  ( y  e.  i  |->  if ( y  =  x ,  1 ,  0 ) ) ,  ( 1r `  r ) ,  ( 0g `  r ) ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  mvrfval  17473  vr1val  17628
  Copyright terms: Public domain W3C validator