Theorem mvrid

Description: The X i -th coefficient of the term X i is 1 . (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	mvrid	|- ( ph -> ( ( V ` X ) ` ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = .1. )

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		1nn0	|- 1 e. NN0
9	2	snifpsrbag	|- ( ( I e. W /\ 1 e. NN0 ) -> ( y e. I |-> if ( y = X , 1 , 0 ) ) e. D )
10	5 8 9	sylancl	|- ( ph -> ( y e. I |-> if ( y = X , 1 , 0 ) ) e. D )
11	1 2 3 4 5 6 7 10	mvrval2	|- ( ph -> ( ( V ` X ) ` ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = if ( ( y e. I |-> if ( y = X , 1 , 0 ) ) = ( y e. I |-> if ( y = X , 1 , 0 ) ) , .1. , .0. ) )
12		eqid	|- ( y e. I |-> if ( y = X , 1 , 0 ) ) = ( y e. I |-> if ( y = X , 1 , 0 ) )
13	12	iftruei	|- if ( ( y e. I |-> if ( y = X , 1 , 0 ) ) = ( y e. I |-> if ( y = X , 1 , 0 ) ) , .1. , .0. ) = .1.
14	11 13	eqtrdi	|- ( ph -> ( ( V ` X ) ` ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = .1. )