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\mathrm{unitVec}I$$
	uvcvv.r	$$⊢\phi \to R\in V$$
	uvcvv.i	$$⊢\phi \to I\in W$$
	uvcvv.j	$$⊢\phi \to J\in I$$
	uvcvv0.k	$$⊢\phi \to K\in I$$
	uvcvv0.jk	$$⊢\phi \to J\ne K$$
	uvcvv0.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	uvcvv0	$$⊢\phi \to U\left(J\right)\left(K\right)=\underset{\dot{}}{0}$$

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		uvcvv0.k	$$⊢\phi \to K\in I$$
6		uvcvv0.jk	$$⊢\phi \to J\ne K$$
7		uvcvv0.z	$$⊢\underset{\dot{}}{0}=0_R$$
8		eqid	$$⊢1_R=1_R$$
9	1 8 7	uvcvval	$$⊢\left(\left(R\in V\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,\underset{\dot{}}{0}\right)$$
10	2 3 4 5 9	syl31anc	$$⊢\phi \to U\left(J\right)\left(K\right)=if\left(K=J,1_R,\underset{\dot{}}{0}\right)$$
11		nesym	$$⊢J\ne K\leftrightarrow \neg K=J$$
12	6 11	sylib	$$⊢\phi \to \neg K=J$$
13	12	iffalsed	$$⊢\phi \to if\left(K=J,1_R,\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
14	10 13	eqtrd	$$⊢\phi \to U\left(J\right)\left(K\right)=\underset{\dot{}}{0}$$