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	⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
	uvcfval.o	⊢ 1 = ( 1r ‘ 𝑅 )
	uvcfval.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	uvcvvcl	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) ∧ 𝐾 ∈ 𝐼 ) → ( ( 𝑈 ‘ 𝐽 ) ‘ 𝐾 ) ∈ { 0 , 1 } )

Proof

Step	Hyp	Ref	Expression
1		uvcfval.u	⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
2		uvcfval.o	⊢ 1 = ( 1r ‘ 𝑅 )
3		uvcfval.z	⊢ 0 = ( 0g ‘ 𝑅 )
4	1 2 3	uvcvval	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) ∧ 𝐾 ∈ 𝐼 ) → ( ( 𝑈 ‘ 𝐽 ) ‘ 𝐾 ) = if ( 𝐾 = 𝐽 , 1 , 0 ) )
5	2	fvexi	⊢ 1 ∈ V
6	3	fvexi	⊢ 0 ∈ V
7		ifpr	⊢ ( ( 1 ∈ V ∧ 0 ∈ V ) → if ( 𝐾 = 𝐽 , 1 , 0 ) ∈ { 1 , 0 } )
8	5 6 7	mp2an	⊢ if ( 𝐾 = 𝐽 , 1 , 0 ) ∈ { 1 , 0 }
9		prcom	⊢ { 1 , 0 } = { 0 , 1 }
10	8 9	eleqtri	⊢ if ( 𝐾 = 𝐽 , 1 , 0 ) ∈ { 0 , 1 }
11	4 10	eqeltrdi	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) ∧ 𝐾 ∈ 𝐼 ) → ( ( 𝑈 ‘ 𝐽 ) ‘ 𝐾 ) ∈ { 0 , 1 } )