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

Metamath Proof Explorer

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