Theorem uvcvvcl

Description: A coordinate of a unit vector is either 0 or 1. (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	uvcvvcl	|- ( ( ( R e. V /\ I e. W /\ J e. I ) /\ K e. I ) -> ( ( U ` J ) ` K ) e. { .0. , .1. } )

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	uvcvval	|- ( ( ( R e. V /\ I e. W /\ J e. I ) /\ K e. I ) -> ( ( U ` J ) ` K ) = if ( K = J , .1. , .0. ) )
5	2	fvexi	|- .1. e. _V
6	3	fvexi	|- .0. e. _V
7		ifpr	|- ( ( .1. e. _V /\ .0. e. _V ) -> if ( K = J , .1. , .0. ) e. { .1. , .0. } )
8	5 6 7	mp2an	|- if ( K = J , .1. , .0. ) e. { .1. , .0. }
9		prcom	|- { .1. , .0. } = { .0. , .1. }
10	8 9	eleqtri	|- if ( K = J , .1. , .0. ) e. { .0. , .1. }
11	4 10	eqeltrdi	|- ( ( ( R e. V /\ I e. W /\ J e. I ) /\ K e. I ) -> ( ( U ` J ) ` K ) e. { .0. , .1. } )