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