Metamath Proof Explorer

Theorem uvcvval

Description: Value of a unit vector coordinate in a free module. (Contributed by Stefan O'Rear, 3-Feb-2015)

Ref Expression
Hypotheses uvcfval.u 
|- U = ( R unitVec I )
uvcfval.o 
|- .1. = ( 1r ` R )
uvcfval.z 
|- .0. = ( 0g ` R )
Assertion uvcvval 
|- ( ( ( R e. V /\ I e. W /\ J e. I ) /\ K e. I ) -> ( ( U ` J ) ` K ) = if ( K = J , .1. , .0. ) )

Proof

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