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

Metamath Proof Explorer

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