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