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

Metamath Proof Explorer

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