Step |
Hyp |
Ref |
Expression |
1 |
|
dvhopsp.s |
⊢ 𝑆 = ( 𝑠 ∈ 𝐸 , 𝑓 ∈ ( 𝑇 × 𝐸 ) ↦ 〈 ( 𝑠 ‘ ( 1st ‘ 𝑓 ) ) , ( 𝑠 ∘ ( 2nd ‘ 𝑓 ) ) 〉 ) |
2 |
|
opelxpi |
⊢ ( ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) → 〈 𝐹 , 𝑈 〉 ∈ ( 𝑇 × 𝐸 ) ) |
3 |
1
|
dvhvscaval |
⊢ ( ( 𝑅 ∈ 𝐸 ∧ 〈 𝐹 , 𝑈 〉 ∈ ( 𝑇 × 𝐸 ) ) → ( 𝑅 𝑆 〈 𝐹 , 𝑈 〉 ) = 〈 ( 𝑅 ‘ ( 1st ‘ 〈 𝐹 , 𝑈 〉 ) ) , ( 𝑅 ∘ ( 2nd ‘ 〈 𝐹 , 𝑈 〉 ) ) 〉 ) |
4 |
2 3
|
sylan2 |
⊢ ( ( 𝑅 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ) → ( 𝑅 𝑆 〈 𝐹 , 𝑈 〉 ) = 〈 ( 𝑅 ‘ ( 1st ‘ 〈 𝐹 , 𝑈 〉 ) ) , ( 𝑅 ∘ ( 2nd ‘ 〈 𝐹 , 𝑈 〉 ) ) 〉 ) |
5 |
|
op1stg |
⊢ ( ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) → ( 1st ‘ 〈 𝐹 , 𝑈 〉 ) = 𝐹 ) |
6 |
5
|
fveq2d |
⊢ ( ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) → ( 𝑅 ‘ ( 1st ‘ 〈 𝐹 , 𝑈 〉 ) ) = ( 𝑅 ‘ 𝐹 ) ) |
7 |
|
op2ndg |
⊢ ( ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) → ( 2nd ‘ 〈 𝐹 , 𝑈 〉 ) = 𝑈 ) |
8 |
7
|
coeq2d |
⊢ ( ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) → ( 𝑅 ∘ ( 2nd ‘ 〈 𝐹 , 𝑈 〉 ) ) = ( 𝑅 ∘ 𝑈 ) ) |
9 |
6 8
|
opeq12d |
⊢ ( ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) → 〈 ( 𝑅 ‘ ( 1st ‘ 〈 𝐹 , 𝑈 〉 ) ) , ( 𝑅 ∘ ( 2nd ‘ 〈 𝐹 , 𝑈 〉 ) ) 〉 = 〈 ( 𝑅 ‘ 𝐹 ) , ( 𝑅 ∘ 𝑈 ) 〉 ) |
10 |
9
|
adantl |
⊢ ( ( 𝑅 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ) → 〈 ( 𝑅 ‘ ( 1st ‘ 〈 𝐹 , 𝑈 〉 ) ) , ( 𝑅 ∘ ( 2nd ‘ 〈 𝐹 , 𝑈 〉 ) ) 〉 = 〈 ( 𝑅 ‘ 𝐹 ) , ( 𝑅 ∘ 𝑈 ) 〉 ) |
11 |
4 10
|
eqtrd |
⊢ ( ( 𝑅 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸 ) ) → ( 𝑅 𝑆 〈 𝐹 , 𝑈 〉 ) = 〈 ( 𝑅 ‘ 𝐹 ) , ( 𝑅 ∘ 𝑈 ) 〉 ) |