Metamath Proof Explorer

Theorem uvcfval

Description: Value of the unit-vector generator for a free module. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Hypotheses uvcfval.u 
|- U = ( R unitVec I )
uvcfval.o 
|- .1. = ( 1r ` R )
uvcfval.z 
|- .0. = ( 0g ` R )
Assertion uvcfval 
|- ( ( R e. V /\ I e. W ) -> U = ( j e. I |-> ( k e. I |-> 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 elex 
 |-  ( R e. V -> R e. _V )
5 elex 
 |-  ( I e. W -> I e. _V )
6 df-uvc 
 |-  unitVec = ( r e. _V , i e. _V |-> ( j e. i |-> ( k e. i |-> if ( k = j , ( 1r ` r ) , ( 0g ` r ) ) ) ) )
7 6 a1i 
 |-  ( ( R e. _V /\ I e. _V ) -> unitVec = ( r e. _V , i e. _V |-> ( j e. i |-> ( k e. i |-> if ( k = j , ( 1r ` r ) , ( 0g ` r ) ) ) ) ) )
8 simpr 
 |-  ( ( r = R /\ i = I ) -> i = I )
9 fveq2 
 |-  ( r = R -> ( 1r ` r ) = ( 1r ` R ) )
10 9 2 eqtr4di 
 |-  ( r = R -> ( 1r ` r ) = .1. )
11 fveq2 
 |-  ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
12 11 3 eqtr4di 
 |-  ( r = R -> ( 0g ` r ) = .0. )
13 10 12 ifeq12d 
 |-  ( r = R -> if ( k = j , ( 1r ` r ) , ( 0g ` r ) ) = if ( k = j , .1. , .0. ) )
14 13 adantr 
 |-  ( ( r = R /\ i = I ) -> if ( k = j , ( 1r ` r ) , ( 0g ` r ) ) = if ( k = j , .1. , .0. ) )
15 8 14 mpteq12dv 
 |-  ( ( r = R /\ i = I ) -> ( k e. i |-> if ( k = j , ( 1r ` r ) , ( 0g ` r ) ) ) = ( k e. I |-> if ( k = j , .1. , .0. ) ) )
16 8 15 mpteq12dv 
 |-  ( ( r = R /\ i = I ) -> ( j e. i |-> ( k e. i |-> if ( k = j , ( 1r ` r ) , ( 0g ` r ) ) ) ) = ( j e. I |-> ( k e. I |-> if ( k = j , .1. , .0. ) ) ) )
17 16 adantl 
 |-  ( ( ( R e. _V /\ I e. _V ) /\ ( r = R /\ i = I ) ) -> ( j e. i |-> ( k e. i |-> if ( k = j , ( 1r ` r ) , ( 0g ` r ) ) ) ) = ( j e. I |-> ( k e. I |-> if ( k = j , .1. , .0. ) ) ) )
18 simpl 
 |-  ( ( R e. _V /\ I e. _V ) -> R e. _V )
19 simpr 
 |-  ( ( R e. _V /\ I e. _V ) -> I e. _V )
20 mptexg 
 |-  ( I e. _V -> ( j e. I |-> ( k e. I |-> if ( k = j , .1. , .0. ) ) ) e. _V )
21 20 adantl 
 |-  ( ( R e. _V /\ I e. _V ) -> ( j e. I |-> ( k e. I |-> if ( k = j , .1. , .0. ) ) ) e. _V )
22 7 17 18 19 21 ovmpod 
 |-  ( ( R e. _V /\ I e. _V ) -> ( R unitVec I ) = ( j e. I |-> ( k e. I |-> if ( k = j , .1. , .0. ) ) ) )
23 4 5 22 syl2an 
 |-  ( ( R e. V /\ I e. W ) -> ( R unitVec I ) = ( j e. I |-> ( k e. I |-> if ( k = j , .1. , .0. ) ) ) )
24 1 23 eqtrid 
 |-  ( ( R e. V /\ I e. W ) -> U = ( j e. I |-> ( k e. I |-> if ( k = j , .1. , .0. ) ) ) )