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. ) )