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

Metamath Proof Explorer

Theorem uvcvvcl2

Description: A unit vector coordinate is a ring element. (Contributed by Stefan O'Rear, 3-Feb-2015)

Ref Expression
Hypotheses uvcvvcl2.u 
|- U = ( R unitVec I )
uvcvvcl2.b 
|- B = ( Base ` R )
uvcvvcl2.r 
|- ( ph -> R e. Ring )
uvcvvcl2.i 
|- ( ph -> I e. W )
uvcvvcl2.j 
|- ( ph -> J e. I )
uvcvvcl2.k 
|- ( ph -> K e. I )
Assertion uvcvvcl2 
|- ( ph -> ( ( U ` J ) ` K ) e. B )

Proof

Step Hyp Ref Expression
1 uvcvvcl2.u 
 |-  U = ( R unitVec I )
2 uvcvvcl2.b 
 |-  B = ( Base ` R )
3 uvcvvcl2.r 
 |-  ( ph -> R e. Ring )
4 uvcvvcl2.i 
 |-  ( ph -> I e. W )
5 uvcvvcl2.j 
 |-  ( ph -> J e. I )
6 uvcvvcl2.k 
 |-  ( ph -> K e. I )
7 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
8 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
9 1 7 8 uvcvval 
 |-  ( ( ( R e. Ring /\ I e. W /\ J e. I ) /\ K e. I ) -> ( ( U ` J ) ` K ) = if ( K = J , ( 1r ` R ) , ( 0g ` R ) ) )
10 3 4 5 6 9 syl31anc 
 |-  ( ph -> ( ( U ` J ) ` K ) = if ( K = J , ( 1r ` R ) , ( 0g ` R ) ) )
11 2 7 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. B )
12 2 8 ring0cl 
 |-  ( R e. Ring -> ( 0g ` R ) e. B )
13 11 12 ifcld 
 |-  ( R e. Ring -> if ( K = J , ( 1r ` R ) , ( 0g ` R ) ) e. B )
14 3 13 syl 
 |-  ( ph -> if ( K = J , ( 1r ` R ) , ( 0g ` R ) ) e. B )
15 10 14 eqeltrd 
 |-  ( ph -> ( ( U ` J ) ` K ) e. B )