Step |
Hyp |
Ref |
Expression |
1 |
|
uvcfval.u |
⊢ 𝑈 = ( 𝑅 unitVec 𝐼 ) |
2 |
|
uvcfval.o |
⊢ 1 = ( 1r ‘ 𝑅 ) |
3 |
|
uvcfval.z |
⊢ 0 = ( 0g ‘ 𝑅 ) |
4 |
1 2 3
|
uvcval |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) → ( 𝑈 ‘ 𝐽 ) = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝐽 , 1 , 0 ) ) ) |
5 |
4
|
fveq1d |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) → ( ( 𝑈 ‘ 𝐽 ) ‘ 𝐾 ) = ( ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝐽 , 1 , 0 ) ) ‘ 𝐾 ) ) |
6 |
5
|
adantr |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) ∧ 𝐾 ∈ 𝐼 ) → ( ( 𝑈 ‘ 𝐽 ) ‘ 𝐾 ) = ( ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝐽 , 1 , 0 ) ) ‘ 𝐾 ) ) |
7 |
|
simpr |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) ∧ 𝐾 ∈ 𝐼 ) → 𝐾 ∈ 𝐼 ) |
8 |
2
|
fvexi |
⊢ 1 ∈ V |
9 |
3
|
fvexi |
⊢ 0 ∈ V |
10 |
8 9
|
ifex |
⊢ if ( 𝐾 = 𝐽 , 1 , 0 ) ∈ V |
11 |
|
eqeq1 |
⊢ ( 𝑘 = 𝐾 → ( 𝑘 = 𝐽 ↔ 𝐾 = 𝐽 ) ) |
12 |
11
|
ifbid |
⊢ ( 𝑘 = 𝐾 → if ( 𝑘 = 𝐽 , 1 , 0 ) = if ( 𝐾 = 𝐽 , 1 , 0 ) ) |
13 |
|
eqid |
⊢ ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝐽 , 1 , 0 ) ) = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝐽 , 1 , 0 ) ) |
14 |
12 13
|
fvmptg |
⊢ ( ( 𝐾 ∈ 𝐼 ∧ if ( 𝐾 = 𝐽 , 1 , 0 ) ∈ V ) → ( ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝐽 , 1 , 0 ) ) ‘ 𝐾 ) = if ( 𝐾 = 𝐽 , 1 , 0 ) ) |
15 |
7 10 14
|
sylancl |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) ∧ 𝐾 ∈ 𝐼 ) → ( ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝐽 , 1 , 0 ) ) ‘ 𝐾 ) = if ( 𝐾 = 𝐽 , 1 , 0 ) ) |
16 |
6 15
|
eqtrd |
⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) ∧ 𝐾 ∈ 𝐼 ) → ( ( 𝑈 ‘ 𝐽 ) ‘ 𝐾 ) = if ( 𝐾 = 𝐽 , 1 , 0 ) ) |