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