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 )