This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } )