Step |
Hyp |
Ref |
Expression |
1 |
|
uvcfval.u |
|- U = ( R unitVec I ) |
2 |
|
uvcfval.o |
|- .1. = ( 1r ` R ) |
3 |
|
uvcfval.z |
|- .0. = ( 0g ` R ) |
4 |
1 2 3
|
uvcval |
|- ( ( R e. V /\ I e. W /\ J e. I ) -> ( U ` J ) = ( k e. I |-> if ( k = J , .1. , .0. ) ) ) |
5 |
4
|
fveq1d |
|- ( ( R e. V /\ I e. W /\ J e. I ) -> ( ( U ` J ) ` K ) = ( ( k e. I |-> if ( k = J , .1. , .0. ) ) ` K ) ) |
6 |
5
|
adantr |
|- ( ( ( R e. V /\ I e. W /\ J e. I ) /\ K e. I ) -> ( ( U ` J ) ` K ) = ( ( k e. I |-> if ( k = J , .1. , .0. ) ) ` K ) ) |
7 |
|
simpr |
|- ( ( ( R e. V /\ I e. W /\ J e. I ) /\ K e. I ) -> K e. I ) |
8 |
2
|
fvexi |
|- .1. e. _V |
9 |
3
|
fvexi |
|- .0. e. _V |
10 |
8 9
|
ifex |
|- if ( K = J , .1. , .0. ) e. _V |
11 |
|
eqeq1 |
|- ( k = K -> ( k = J <-> K = J ) ) |
12 |
11
|
ifbid |
|- ( k = K -> if ( k = J , .1. , .0. ) = if ( K = J , .1. , .0. ) ) |
13 |
|
eqid |
|- ( k e. I |-> if ( k = J , .1. , .0. ) ) = ( k e. I |-> if ( k = J , .1. , .0. ) ) |
14 |
12 13
|
fvmptg |
|- ( ( K e. I /\ if ( K = J , .1. , .0. ) e. _V ) -> ( ( k e. I |-> if ( k = J , .1. , .0. ) ) ` K ) = if ( K = J , .1. , .0. ) ) |
15 |
7 10 14
|
sylancl |
|- ( ( ( R e. V /\ I e. W /\ J e. I ) /\ K e. I ) -> ( ( k e. I |-> if ( k = J , .1. , .0. ) ) ` K ) = if ( K = J , .1. , .0. ) ) |
16 |
6 15
|
eqtrd |
|- ( ( ( R e. V /\ I e. W /\ J e. I ) /\ K e. I ) -> ( ( U ` J ) ` K ) = if ( K = J , .1. , .0. ) ) |