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

Definition df-mvr 16410
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 16399 . 2  class mVar
2 vi . . 3  set  i
3 vr . . 3  set  r
4 cvv 2948 . . 3  class  _V
5 vx . . . 4  set  x
62cv 1651 . . . 4  class  i
7 vf . . . . 5  set  f
8 vh . . . . . . . . . 10  set  h
98cv 1651 . . . . . . . . 9  class  h
109ccnv 4869 . . . . . . . 8  class  `' h
11 cn 9992 . . . . . . . 8  class  NN
1210, 11cima 4873 . . . . . . 7  class  ( `' h " NN )
13 cfn 7101 . . . . . . 7  class  Fin
1412, 13wcel 1725 . . . . . 6  wff  ( `' h " NN )  e.  Fin
15 cn0 10213 . . . . . . 7  class  NN0
16 cmap 7010 . . . . . . 7  class  ^m
1715, 6, 16co 6073 . . . . . 6  class  ( NN0 
^m  i )
1814, 8, 17crab 2701 . . . . 5  class  { h  e.  ( NN0  ^m  i
)  |  ( `' h " NN )  e.  Fin }
197cv 1651 . . . . . . 7  class  f
20 vy . . . . . . . 8  set  y
2120, 5weq 1653 . . . . . . . . 9  wff  y  =  x
22 c1 8983 . . . . . . . . 9  class  1
23 cc0 8982 . . . . . . . . 9  class  0
2421, 22, 23cif 3731 . . . . . . . 8  class  if ( y  =  x ,  1 ,  0 )
2520, 6, 24cmpt 4258 . . . . . . 7  class  ( y  e.  i  |->  if ( y  =  x ,  1 ,  0 ) )
2619, 25wceq 1652 . . . . . 6  wff  f  =  ( y  e.  i 
|->  if ( y  =  x ,  1 ,  0 ) )
273cv 1651 . . . . . . 7  class  r
28 cur 15654 . . . . . . 7  class  1r
2927, 28cfv 5446 . . . . . 6  class  ( 1r
`  r )
30 c0g 13715 . . . . . . 7  class  0g
3127, 30cfv 5446 . . . . . 6  class  ( 0g
`  r )
3226, 29, 31cif 3731 . . . . 5  class  if ( f  =  ( y  e.  i  |->  if ( y  =  x ,  1 ,  0 ) ) ,  ( 1r
`  r ) ,  ( 0g `  r
) )
337, 18, 32cmpt 4258 . . . 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 4258 . . 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 6075 . 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 1652 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  16476  vr1val  16582
  Copyright terms: Public domain W3C validator