Step |
Hyp |
Ref |
Expression |
1 |
|
dvhvscaval.s |
⊢ · = ( 𝑠 ∈ 𝐸 , 𝑓 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) |
2 |
|
fveq1 |
⊢ ( 𝑡 = 𝑈 → ( 𝑡 ‘ ( 1st ‘ 𝑔 ) ) = ( 𝑈 ‘ ( 1st ‘ 𝑔 ) ) ) |
3 |
|
coeq1 |
⊢ ( 𝑡 = 𝑈 → ( 𝑡 ∘ ( 2nd ‘ 𝑔 ) ) = ( 𝑈 ∘ ( 2nd ‘ 𝑔 ) ) ) |
4 |
2 3
|
opeq12d |
⊢ ( 𝑡 = 𝑈 → 〈 ( 𝑡 ‘ ( 1st ‘ 𝑔 ) ) , ( 𝑡 ∘ ( 2nd ‘ 𝑔 ) ) 〉 = 〈 ( 𝑈 ‘ ( 1st ‘ 𝑔 ) ) , ( 𝑈 ∘ ( 2nd ‘ 𝑔 ) ) 〉 ) |
5 |
|
2fveq3 |
⊢ ( 𝑔 = 𝐹 → ( 𝑈 ‘ ( 1st ‘ 𝑔 ) ) = ( 𝑈 ‘ ( 1st ‘ 𝐹 ) ) ) |
6 |
|
fveq2 |
⊢ ( 𝑔 = 𝐹 → ( 2nd ‘ 𝑔 ) = ( 2nd ‘ 𝐹 ) ) |
7 |
6
|
coeq2d |
⊢ ( 𝑔 = 𝐹 → ( 𝑈 ∘ ( 2nd ‘ 𝑔 ) ) = ( 𝑈 ∘ ( 2nd ‘ 𝐹 ) ) ) |
8 |
5 7
|
opeq12d |
⊢ ( 𝑔 = 𝐹 → 〈 ( 𝑈 ‘ ( 1st ‘ 𝑔 ) ) , ( 𝑈 ∘ ( 2nd ‘ 𝑔 ) ) 〉 = 〈 ( 𝑈 ‘ ( 1st ‘ 𝐹 ) ) , ( 𝑈 ∘ ( 2nd ‘ 𝐹 ) ) 〉 ) |
9 |
1
|
dvhvscacbv |
⊢ · = ( 𝑡 ∈ 𝐸 , 𝑔 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( 𝑡 ‘ ( 1st ‘ 𝑔 ) ) , ( 𝑡 ∘ ( 2nd ‘ 𝑔 ) ) 〉 ) |
10 |
|
opex |
⊢ 〈 ( 𝑈 ‘ ( 1st ‘ 𝐹 ) ) , ( 𝑈 ∘ ( 2nd ‘ 𝐹 ) ) 〉 ∈ V |
11 |
4 8 9 10
|
ovmpo |
⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝐹 ∈ ( 𝑇 × 𝐸 ) ) → ( 𝑈 · 𝐹 ) = 〈 ( 𝑈 ‘ ( 1st ‘ 𝐹 ) ) , ( 𝑈 ∘ ( 2nd ‘ 𝐹 ) ) 〉 ) |