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 unitVec I$
	uvcfval.o	$⊢ \underset{˙}{1} = 1_{R}$
	uvcfval.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	uvcvvcl	$⊢ ((R \in V \land I \in W \land J \in I) \land K \in I) \to U (J) (K) \in \{\underset{˙}{0}, \underset{˙}{1}\}$

Step	Hyp	Ref	Expression
1		uvcfval.u	$⊢ U = R unitVec I$
2		uvcfval.o	$⊢ \underset{˙}{1} = 1_{R}$
3		uvcfval.z	$⊢ \underset{˙}{0} = 0_{R}$
4	1 2 3	uvcvval	$⊢ ((R \in V \land I \in W \land J \in I) \land K \in I) \to U (J) (K) = if (K = J, \underset{˙}{1}, \underset{˙}{0})$
5	2	fvexi	$⊢ \underset{˙}{1} \in V$
6	3	fvexi	$⊢ \underset{˙}{0} \in V$
7		ifpr	$⊢ (\underset{˙}{1} \in V \land \underset{˙}{0} \in V) \to if (K = J, \underset{˙}{1}, \underset{˙}{0}) \in \{\underset{˙}{1}, \underset{˙}{0}\}$
8	5 6 7	mp2an	$⊢ if (K = J, \underset{˙}{1}, \underset{˙}{0}) \in \{\underset{˙}{1}, \underset{˙}{0}\}$
9		prcom	$⊢ \{\underset{˙}{1}, \underset{˙}{0}\} = \{\underset{˙}{0}, \underset{˙}{1}\}$
10	8 9	eleqtri	$⊢ if (K = J, \underset{˙}{1}, \underset{˙}{0}) \in \{\underset{˙}{0}, \underset{˙}{1}\}$
11	4 10	eqeltrdi	$⊢ ((R \in V \land I \in W \land J \in I) \land K \in I) \to U (J) (K) \in \{\underset{˙}{0}, \underset{˙}{1}\}$

Metamath Proof Explorer