Metamath Proof Explorer

Definition df-mvr

Description: Define the generating elements of the power series algebra. (Contributed by Mario Carneiro, 7-Jan-2015)

Ref Expression
Assertion 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 ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmvr 
 |-  mVar
1 vi 
 |-  i
2 cvv 
 |-  _V
3 vr 
 |-  r
4 vx 
 |-  x
5 1 cv 
 |-  i
6 vf 
 |-  f
7 vh 
 |-  h
8 cn0 
 |-  NN0
9 cmap 
 |-  ^m
10 8 5 9 co 
 |-  ( NN0 ^m i )
11 7 cv 
 |-  h
12 11 ccnv 
 |-  `' h
13 cn 
 |-  NN
14 12 13 cima 
 |-  ( `' h " NN )
15 cfn 
 |-  Fin
16 14 15 wcel 
 |-  ( `' h " NN ) e. Fin
17 16 7 10 crab 
 |-  { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin }
18 6 cv 
 |-  f
19 vy 
 |-  y
20 19 cv 
 |-  y
21 4 cv 
 |-  x
22 20 21 wceq 
 |-  y = x
23 c1 
 |-  1
24 cc0 
 |-  0
25 22 23 24 cif 
 |-  if ( y = x , 1 , 0 )
26 19 5 25 cmpt 
 |-  ( y e. i |-> if ( y = x , 1 , 0 ) )
27 18 26 wceq 
 |-  f = ( y e. i |-> if ( y = x , 1 , 0 ) )
28 cur 
 |-  1r
29 3 cv 
 |-  r
30 29 28 cfv 
 |-  ( 1r ` r )
31 c0g 
 |-  0g
32 29 31 cfv 
 |-  ( 0g ` r )
33 27 30 32 cif 
 |-  if ( f = ( y e. i |-> if ( y = x , 1 , 0 ) ) , ( 1r ` r ) , ( 0g ` r ) )
34 6 17 33 cmpt 
 |-  ( 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 ) ) )
35 4 5 34 cmpt 
 |-  ( 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 ) ) ) )
36 1 3 2 2 35 cmpo 
 |-  ( 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 ) ) ) ) )
37 0 36 wceq 
 |-  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 ) ) ) ) )