Step |
Hyp |
Ref |
Expression |
1 |
|
uvcvvcl2.u |
⊢ 𝑈 = ( 𝑅 unitVec 𝐼 ) |
2 |
|
uvcvvcl2.b |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
3 |
|
uvcvvcl2.r |
⊢ ( 𝜑 → 𝑅 ∈ Ring ) |
4 |
|
uvcvvcl2.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑊 ) |
5 |
|
uvcvvcl2.j |
⊢ ( 𝜑 → 𝐽 ∈ 𝐼 ) |
6 |
|
uvcvvcl2.k |
⊢ ( 𝜑 → 𝐾 ∈ 𝐼 ) |
7 |
|
eqid |
⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) |
8 |
|
eqid |
⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) |
9 |
1 7 8
|
uvcvval |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) ∧ 𝐾 ∈ 𝐼 ) → ( ( 𝑈 ‘ 𝐽 ) ‘ 𝐾 ) = if ( 𝐾 = 𝐽 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) |
10 |
3 4 5 6 9
|
syl31anc |
⊢ ( 𝜑 → ( ( 𝑈 ‘ 𝐽 ) ‘ 𝐾 ) = if ( 𝐾 = 𝐽 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) |
11 |
2 7
|
ringidcl |
⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 ) |
12 |
2 8
|
ring0cl |
⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝑅 ) ∈ 𝐵 ) |
13 |
11 12
|
ifcld |
⊢ ( 𝑅 ∈ Ring → if ( 𝐾 = 𝐽 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ 𝐵 ) |
14 |
3 13
|
syl |
⊢ ( 𝜑 → if ( 𝐾 = 𝐽 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ 𝐵 ) |
15 |
10 14
|
eqeltrd |
⊢ ( 𝜑 → ( ( 𝑈 ‘ 𝐽 ) ‘ 𝐾 ) ∈ 𝐵 ) |