Theorem uvcvv1

Description: The unit vector is one at its designated coordinate. (Contributed by Stefan O'Rear, 3-Feb-2015)

	Ref	Expression
Hypotheses	uvcvv.u	|- U = ( R unitVec I )
	uvcvv.r	|- ( ph -> R e. V )
	uvcvv.i	|- ( ph -> I e. W )
	uvcvv.j	|- ( ph -> J e. I )
	uvcvv1.o	|- .1. = ( 1r ` R )
Assertion	uvcvv1	|- ( ph -> ( ( U ` J ) ` J ) = .1. )

Proof

Step	Hyp	Ref	Expression
1		uvcvv.u	|- U = ( R unitVec I )
2		uvcvv.r	|- ( ph -> R e. V )
3		uvcvv.i	|- ( ph -> I e. W )
4		uvcvv.j	|- ( ph -> J e. I )
5		uvcvv1.o	|- .1. = ( 1r ` R )
6		eqid	|- ( 0g ` R ) = ( 0g ` R )
7	1 5 6	uvcvval	|- ( ( ( R e. V /\ I e. W /\ J e. I ) /\ J e. I ) -> ( ( U ` J ) ` J ) = if ( J = J , .1. , ( 0g ` R ) ) )
8	2 3 4 4 7	syl31anc	|- ( ph -> ( ( U ` J ) ` J ) = if ( J = J , .1. , ( 0g ` R ) ) )
9		eqid	|- J = J
10		iftrue	|- ( J = J -> if ( J = J , .1. , ( 0g ` R ) ) = .1. )
11	9 10	mp1i	|- ( ph -> if ( J = J , .1. , ( 0g ` R ) ) = .1. )
12	8 11	eqtrd	|- ( ph -> ( ( U ` J ) ` J ) = .1. )