Step |
Hyp |
Ref |
Expression |
1 |
|
fveq2 |
⊢ ( 𝑥 = 𝐴 → ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝐴 ) ) |
2 |
1
|
oveq1d |
⊢ ( 𝑥 = 𝐴 → ( ( 1st ‘ 𝑥 ) ·N ( 1st ‘ 𝑦 ) ) = ( ( 1st ‘ 𝐴 ) ·N ( 1st ‘ 𝑦 ) ) ) |
3 |
|
fveq2 |
⊢ ( 𝑥 = 𝐴 → ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝐴 ) ) |
4 |
3
|
oveq1d |
⊢ ( 𝑥 = 𝐴 → ( ( 2nd ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) = ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝑦 ) ) ) |
5 |
2 4
|
opeq12d |
⊢ ( 𝑥 = 𝐴 → 〈 ( ( 1st ‘ 𝑥 ) ·N ( 1st ‘ 𝑦 ) ) , ( ( 2nd ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) 〉 = 〈 ( ( 1st ‘ 𝐴 ) ·N ( 1st ‘ 𝑦 ) ) , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝑦 ) ) 〉 ) |
6 |
|
fveq2 |
⊢ ( 𝑦 = 𝐵 → ( 1st ‘ 𝑦 ) = ( 1st ‘ 𝐵 ) ) |
7 |
6
|
oveq2d |
⊢ ( 𝑦 = 𝐵 → ( ( 1st ‘ 𝐴 ) ·N ( 1st ‘ 𝑦 ) ) = ( ( 1st ‘ 𝐴 ) ·N ( 1st ‘ 𝐵 ) ) ) |
8 |
|
fveq2 |
⊢ ( 𝑦 = 𝐵 → ( 2nd ‘ 𝑦 ) = ( 2nd ‘ 𝐵 ) ) |
9 |
8
|
oveq2d |
⊢ ( 𝑦 = 𝐵 → ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝑦 ) ) = ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) |
10 |
7 9
|
opeq12d |
⊢ ( 𝑦 = 𝐵 → 〈 ( ( 1st ‘ 𝐴 ) ·N ( 1st ‘ 𝑦 ) ) , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝑦 ) ) 〉 = 〈 ( ( 1st ‘ 𝐴 ) ·N ( 1st ‘ 𝐵 ) ) , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) 〉 ) |
11 |
|
df-mpq |
⊢ ·pQ = ( 𝑥 ∈ ( N × N ) , 𝑦 ∈ ( N × N ) ↦ 〈 ( ( 1st ‘ 𝑥 ) ·N ( 1st ‘ 𝑦 ) ) , ( ( 2nd ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) 〉 ) |
12 |
|
opex |
⊢ 〈 ( ( 1st ‘ 𝐴 ) ·N ( 1st ‘ 𝐵 ) ) , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) 〉 ∈ V |
13 |
5 10 11 12
|
ovmpo |
⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 ·pQ 𝐵 ) = 〈 ( ( 1st ‘ 𝐴 ) ·N ( 1st ‘ 𝐵 ) ) , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) 〉 ) |