Metamath Proof Explorer


Theorem mvrval2

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 )
mvrval2.f
|- ( ph -> F e. D )
Assertion mvrval2
|- ( ph -> ( ( V ` X ) ` F ) = 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 mvrval2.f
 |-  ( ph -> F e. D )
9 1 2 3 4 5 6 7 mvrval
 |-  ( ph -> ( V ` X ) = ( f e. D |-> if ( f = ( y e. I |-> if ( y = X , 1 , 0 ) ) , .1. , .0. ) ) )
10 9 fveq1d
 |-  ( ph -> ( ( V ` X ) ` F ) = ( ( f e. D |-> if ( f = ( y e. I |-> if ( y = X , 1 , 0 ) ) , .1. , .0. ) ) ` F ) )
11 eqeq1
 |-  ( f = F -> ( f = ( y e. I |-> if ( y = X , 1 , 0 ) ) <-> F = ( y e. I |-> if ( y = X , 1 , 0 ) ) ) )
12 11 ifbid
 |-  ( f = F -> if ( f = ( y e. I |-> if ( y = X , 1 , 0 ) ) , .1. , .0. ) = if ( F = ( y e. I |-> if ( y = X , 1 , 0 ) ) , .1. , .0. ) )
13 eqid
 |-  ( 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. ) )
14 4 fvexi
 |-  .1. e. _V
15 3 fvexi
 |-  .0. e. _V
16 14 15 ifex
 |-  if ( F = ( y e. I |-> if ( y = X , 1 , 0 ) ) , .1. , .0. ) e. _V
17 12 13 16 fvmpt
 |-  ( F e. D -> ( ( f e. D |-> if ( f = ( y e. I |-> if ( y = X , 1 , 0 ) ) , .1. , .0. ) ) ` F ) = if ( F = ( y e. I |-> if ( y = X , 1 , 0 ) ) , .1. , .0. ) )
18 8 17 syl
 |-  ( ph -> ( ( f e. D |-> if ( f = ( y e. I |-> if ( y = X , 1 , 0 ) ) , .1. , .0. ) ) ` F ) = if ( F = ( y e. I |-> if ( y = X , 1 , 0 ) ) , .1. , .0. ) )
19 10 18 eqtrd
 |-  ( ph -> ( ( V ` X ) ` F ) = if ( F = ( y e. I |-> if ( y = X , 1 , 0 ) ) , .1. , .0. ) )