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