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

Definition df-mvr 16099
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 16088 . 2  class mVar
2 vi . . 3  set  i
3 vr . . 3  set  r
4 cvv 2788 . . 3  class  _V
5 vx . . . 4  set  x
62cv 1622 . . . 4  class  i
7 vf . . . . 5  set  f
8 vh . . . . . . . . . 10  set  h
98cv 1622 . . . . . . . . 9  class  h
109ccnv 4688 . . . . . . . 8  class  `' h
11 cn 9746 . . . . . . . 8  class  NN
1210, 11cima 4692 . . . . . . 7  class  ( `' h " NN )
13 cfn 6863 . . . . . . 7  class  Fin
1412, 13wcel 1684 . . . . . 6  wff  ( `' h " NN )  e.  Fin
15 cn0 9965 . . . . . . 7  class  NN0
16 cmap 6772 . . . . . . 7  class  ^m
1715, 6, 16co 5858 . . . . . 6  class  ( NN0 
^m  i )
1814, 8, 17crab 2547 . . . . 5  class  { h  e.  ( NN0  ^m  i
)  |  ( `' h " NN )  e.  Fin }
197cv 1622 . . . . . . 7  class  f
20 vy . . . . . . . 8  set  y
2120, 5weq 1624 . . . . . . . . 9  wff  y  =  x
22 c1 8738 . . . . . . . . 9  class  1
23 cc0 8737 . . . . . . . . 9  class  0
2421, 22, 23cif 3565 . . . . . . . 8  class  if ( y  =  x ,  1 ,  0 )
2520, 6, 24cmpt 4077 . . . . . . 7  class  ( y  e.  i  |->  if ( y  =  x ,  1 ,  0 ) )
2619, 25wceq 1623 . . . . . 6  wff  f  =  ( y  e.  i 
|->  if ( y  =  x ,  1 ,  0 ) )
273cv 1622 . . . . . . 7  class  r
28 cur 15339 . . . . . . 7  class  1r
2927, 28cfv 5255 . . . . . 6  class  ( 1r
`  r )
30 c0g 13400 . . . . . . 7  class  0g
3127, 30cfv 5255 . . . . . 6  class  ( 0g
`  r )
3226, 29, 31cif 3565 . . . . 5  class  if ( f  =  ( y  e.  i  |->  if ( y  =  x ,  1 ,  0 ) ) ,  ( 1r
`  r ) ,  ( 0g `  r
) )
337, 18, 32cmpt 4077 . . . 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 4077 . . 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 5860 . 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 1623 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 set class
This definition is referenced by:  mvrfval  16165  vr1val  16271
  Copyright terms: Public domain W3C validator