Theorem uvcvvcl

Description: A coordinate of a unit vector is either 0 or 1. (Contributed by Stefan O'Rear, 3-Feb-2015)

	Ref	Expression
Hypotheses	uvcfval.u	$$⊢U=R\mathrm{unitVec}I$$
	uvcfval.o	$$⊢\underset{\dot{}}{1}=1_R$$
	uvcfval.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	uvcvvcl	$$⊢\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)\in \left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		uvcfval.u	$$⊢U=R\mathrm{unitVec}I$$
2		uvcfval.o	$$⊢\underset{\dot{}}{1}=1_R$$
3		uvcfval.z	$$⊢\underset{\dot{}}{0}=0_R$$
4	1 2 3	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,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
5	2	fvexi	$$⊢\underset{\dot{}}{1}\in \mathrm{V}$$
6	3	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
7		ifpr	$$⊢\left(\underset{\dot{}}{1}\in \mathrm{V}\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)\to if\left(K=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in \left\{\underset{\dot{}}{1},\underset{\dot{}}{0}\right\}$$
8	5 6 7	mp2an	$$⊢if\left(K=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in \left\{\underset{\dot{}}{1},\underset{\dot{}}{0}\right\}$$
9		prcom	$$⊢\left\{\underset{\dot{}}{1},\underset{\dot{}}{0}\right\}=\left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}$$
10	8 9	eleqtri	$$⊢if\left(K=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in \left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}$$
11	4 10	eqeltrdi	$$⊢\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)\in \left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}$$