Theorem uvcvv1

Description: The unit vector is one at its designated coordinate. (Contributed by Stefan O'Rear, 3-Feb-2015)

	Ref	Expression
Hypotheses	uvcvv.u	$$⊢U=R\mathrm{unitVec}I$$
	uvcvv.r	$$⊢\phi \to R\in V$$
	uvcvv.i	$$⊢\phi \to I\in W$$
	uvcvv.j	$$⊢\phi \to J\in I$$
	uvcvv1.o	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	uvcvv1	$$⊢\phi \to U\left(J\right)\left(J\right)=\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		uvcvv.u	$$⊢U=R\mathrm{unitVec}I$$
2		uvcvv.r	$$⊢\phi \to R\in V$$
3		uvcvv.i	$$⊢\phi \to I\in W$$
4		uvcvv.j	$$⊢\phi \to J\in I$$
5		uvcvv1.o	$$⊢\underset{\dot{}}{1}=1_R$$
6		eqid	$$⊢0_R=0_R$$
7	1 5 6	uvcvval	$$⊢\left(\left(R\in V\wedge I\in W\wedge J\in I\right)\wedge J\in I\right)\to U\left(J\right)\left(J\right)=if\left(J=J,\underset{\dot{}}{1},0_R\right)$$
8	2 3 4 4 7	syl31anc	$$⊢\phi \to U\left(J\right)\left(J\right)=if\left(J=J,\underset{\dot{}}{1},0_R\right)$$
9		eqid	$$⊢J=J$$
10		iftrue	$$⊢J=J\to if\left(J=J,\underset{\dot{}}{1},0_R\right)=\underset{\dot{}}{1}$$
11	9 10	mp1i	$$⊢\phi \to if\left(J=J,\underset{\dot{}}{1},0_R\right)=\underset{\dot{}}{1}$$
12	8 11	eqtrd	$$⊢\phi \to U\left(J\right)\left(J\right)=\underset{\dot{}}{1}$$