This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mvrval

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

Ref Expression
Hypotheses mvrfval.v 
|- V = ( I mVar R )
mvrfval.d 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
mvrfval.z 
|- .0. = ( 0g ` R )
mvrfval.o 
|- .1. = ( 1r ` R )
mvrfval.i 
|- ( ph -> I e. W )
mvrfval.r 
|- ( ph -> R e. Y )
mvrval.x 
|- ( ph -> X e. I )
Assertion mvrval 
|- ( ph -> ( V ` X ) = ( f e. D |-> if ( f = ( y e. I |-> if ( y = X , 1 , 0 ) ) , .1. , .0. ) ) )

Proof

Step Hyp Ref Expression
1 mvrfval.v 
 |-  V = ( I mVar R )
2 mvrfval.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
3 mvrfval.z 
 |-  .0. = ( 0g ` R )
4 mvrfval.o 
 |-  .1. = ( 1r ` R )
5 mvrfval.i 
 |-  ( ph -> I e. W )
6 mvrfval.r 
 |-  ( ph -> R e. Y )
7 mvrval.x 
 |-  ( ph -> X e. I )
8 1 2 3 4 5 6 mvrfval 
 |-  ( ph -> V = ( x e. I |-> ( f e. D |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , .1. , .0. ) ) ) )
9 8 fveq1d 
 |-  ( ph -> ( V ` X ) = ( ( x e. I |-> ( f e. D |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , .1. , .0. ) ) ) ` X ) )
10 eqeq2 
 |-  ( x = X -> ( y = x <-> y = X ) )
11 10 ifbid 
 |-  ( x = X -> if ( y = x , 1 , 0 ) = if ( y = X , 1 , 0 ) )
12 11 mpteq2dv 
 |-  ( x = X -> ( y e. I |-> if ( y = x , 1 , 0 ) ) = ( y e. I |-> if ( y = X , 1 , 0 ) ) )
13 12 eqeq2d 
 |-  ( x = X -> ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) <-> f = ( y e. I |-> if ( y = X , 1 , 0 ) ) ) )
14 13 ifbid 
 |-  ( x = X -> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , .1. , .0. ) = if ( f = ( y e. I |-> if ( y = X , 1 , 0 ) ) , .1. , .0. ) )
15 14 mpteq2dv 
 |-  ( x = X -> ( f e. D |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , .1. , .0. ) ) = ( f e. D |-> if ( f = ( y e. I |-> if ( y = X , 1 , 0 ) ) , .1. , .0. ) ) )
16 eqid 
 |-  ( x e. I |-> ( f e. D |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , .1. , .0. ) ) ) = ( x e. I |-> ( f e. D |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , .1. , .0. ) ) )
17 ovex 
 |-  ( NN0 ^m I ) e. _V
18 2 17 rabex2 
 |-  D e. _V
19 18 mptex 
 |-  ( f e. D |-> if ( f = ( y e. I |-> if ( y = X , 1 , 0 ) ) , .1. , .0. ) ) e. _V
20 15 16 19 fvmpt 
 |-  ( X e. I -> ( ( x e. I |-> ( f e. D |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , .1. , .0. ) ) ) ` X ) = ( f e. D |-> if ( f = ( y e. I |-> if ( y = X , 1 , 0 ) ) , .1. , .0. ) ) )
21 7 20 syl 
 |-  ( ph -> ( ( x e. I |-> ( f e. D |-> if ( f = ( y e. I |-> if ( y = x , 1 , 0 ) ) , .1. , .0. ) ) ) ` X ) = ( f e. D |-> if ( f = ( y e. I |-> if ( y = X , 1 , 0 ) ) , .1. , .0. ) ) )
22 9 21 eqtrd 
 |-  ( ph -> ( V ` X ) = ( f e. D |-> if ( f = ( y e. I |-> if ( y = X , 1 , 0 ) ) , .1. , .0. ) ) )