This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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. } )