Theorem uvcvv0

Description: The unit vector is zero 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 )
	uvcvv0.k	|- ( ph -> K e. I )
	uvcvv0.jk	|- ( ph -> J =/= K )
	uvcvv0.z	|- .0. = ( 0g ` R )
Assertion	uvcvv0	|- ( ph -> ( ( U ` J ) ` K ) = .0. )

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		uvcvv0.k	|- ( ph -> K e. I )
6		uvcvv0.jk	|- ( ph -> J =/= K )
7		uvcvv0.z	|- .0. = ( 0g ` R )
8		eqid	|- ( 1r ` R ) = ( 1r ` R )
9	1 8 7	uvcvval	|- ( ( ( R e. V /\ I e. W /\ J e. I ) /\ K e. I ) -> ( ( U ` J ) ` K ) = if ( K = J , ( 1r ` R ) , .0. ) )
10	2 3 4 5 9	syl31anc	|- ( ph -> ( ( U ` J ) ` K ) = if ( K = J , ( 1r ` R ) , .0. ) )
11		nesym	|- ( J =/= K <-> -. K = J )
12	6 11	sylib	|- ( ph -> -. K = J )
13	12	iffalsed	|- ( ph -> if ( K = J , ( 1r ` R ) , .0. ) = .0. )
14	10 13	eqtrd	|- ( ph -> ( ( U ` J ) ` K ) = .0. )