Theorem uvcval

Description: Value of a single unit vector 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	uvcval	|- ( ( R e. V /\ I e. W /\ J e. I ) -> ( U ` J ) = ( 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	1 2 3	uvcfval	|- ( ( R e. V /\ I e. W ) -> U = ( j e. I |-> ( k e. I |-> if ( k = j , .1. , .0. ) ) ) )
5	4	fveq1d	|- ( ( R e. V /\ I e. W ) -> ( U ` J ) = ( ( j e. I |-> ( k e. I |-> if ( k = j , .1. , .0. ) ) ) ` J ) )
6	5	3adant3	|- ( ( R e. V /\ I e. W /\ J e. I ) -> ( U ` J ) = ( ( j e. I |-> ( k e. I |-> if ( k = j , .1. , .0. ) ) ) ` J ) )
7		eqid	|- ( j e. I |-> ( k e. I |-> if ( k = j , .1. , .0. ) ) ) = ( j e. I |-> ( k e. I |-> if ( k = j , .1. , .0. ) ) )
8		eqeq2	|- ( j = J -> ( k = j <-> k = J ) )
9	8	ifbid	|- ( j = J -> if ( k = j , .1. , .0. ) = if ( k = J , .1. , .0. ) )
10	9	mpteq2dv	|- ( j = J -> ( k e. I |-> if ( k = j , .1. , .0. ) ) = ( k e. I |-> if ( k = J , .1. , .0. ) ) )
11		simp3	|- ( ( R e. V /\ I e. W /\ J e. I ) -> J e. I )
12		mptexg	|- ( I e. W -> ( k e. I |-> if ( k = J , .1. , .0. ) ) e. _V )
13	12	3ad2ant2	|- ( ( R e. V /\ I e. W /\ J e. I ) -> ( k e. I |-> if ( k = J , .1. , .0. ) ) e. _V )
14	7 10 11 13	fvmptd3	|- ( ( R e. V /\ I e. W /\ J e. I ) -> ( ( j e. I |-> ( k e. I |-> if ( k = j , .1. , .0. ) ) ) ` J ) = ( k e. I |-> if ( k = J , .1. , .0. ) ) )
15	6 14	eqtrd	|- ( ( R e. V /\ I e. W /\ J e. I ) -> ( U ` J ) = ( k e. I |-> if ( k = J , .1. , .0. ) ) )