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\mathrm{unitVec}I$$
	uvcvvcl2.b	$$⊢B={\mathrm{Base}}_R$$
	uvcvvcl2.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	uvcvvcl2.i	$$⊢\phi \to I\in W$$
	uvcvvcl2.j	$$⊢\phi \to J\in I$$
	uvcvvcl2.k	$$⊢\phi \to K\in I$$
Assertion	uvcvvcl2	$$⊢\phi \to U\left(J\right)\left(K\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		uvcvvcl2.u	$$⊢U=R\mathrm{unitVec}I$$
2		uvcvvcl2.b	$$⊢B={\mathrm{Base}}_R$$
3		uvcvvcl2.r	$$⊢\phi \to R\in \mathrm{Ring}$$
4		uvcvvcl2.i	$$⊢\phi \to I\in W$$
5		uvcvvcl2.j	$$⊢\phi \to J\in I$$
6		uvcvvcl2.k	$$⊢\phi \to K\in I$$
7		eqid	$$⊢1_R=1_R$$
8		eqid	$$⊢0_R=0_R$$
9	1 7 8	uvcvval	$$⊢\left(\left(R\in \mathrm{Ring}\wedge I\in W\wedge J\in I\right)\wedge K\in I\right)\to U\left(J\right)\left(K\right)=if\left(K=J,1_R,0_R\right)$$
10	3 4 5 6 9	syl31anc	$$⊢\phi \to U\left(J\right)\left(K\right)=if\left(K=J,1_R,0_R\right)$$
11	2 7	ringidcl	$$⊢R\in \mathrm{Ring}\to 1_R\in B$$
12	2 8	ring0cl	$$⊢R\in \mathrm{Ring}\to 0_R\in B$$
13	11 12	ifcld	$$⊢R\in \mathrm{Ring}\to if\left(K=J,1_R,0_R\right)\in B$$
14	3 13	syl	$$⊢\phi \to if\left(K=J,1_R,0_R\right)\in B$$
15	10 14	eqeltrd	$$⊢\phi \to U\left(J\right)\left(K\right)\in B$$