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