Step |
Hyp |
Ref |
Expression |
1 |
|
fveq2 |
|- ( x = A -> ( 1st ` x ) = ( 1st ` A ) ) |
2 |
1
|
oveq1d |
|- ( x = A -> ( ( 1st ` x ) .N ( 1st ` y ) ) = ( ( 1st ` A ) .N ( 1st ` y ) ) ) |
3 |
|
fveq2 |
|- ( x = A -> ( 2nd ` x ) = ( 2nd ` A ) ) |
4 |
3
|
oveq1d |
|- ( x = A -> ( ( 2nd ` x ) .N ( 2nd ` y ) ) = ( ( 2nd ` A ) .N ( 2nd ` y ) ) ) |
5 |
2 4
|
opeq12d |
|- ( x = A -> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. = <. ( ( 1st ` A ) .N ( 1st ` y ) ) , ( ( 2nd ` A ) .N ( 2nd ` y ) ) >. ) |
6 |
|
fveq2 |
|- ( y = B -> ( 1st ` y ) = ( 1st ` B ) ) |
7 |
6
|
oveq2d |
|- ( y = B -> ( ( 1st ` A ) .N ( 1st ` y ) ) = ( ( 1st ` A ) .N ( 1st ` B ) ) ) |
8 |
|
fveq2 |
|- ( y = B -> ( 2nd ` y ) = ( 2nd ` B ) ) |
9 |
8
|
oveq2d |
|- ( y = B -> ( ( 2nd ` A ) .N ( 2nd ` y ) ) = ( ( 2nd ` A ) .N ( 2nd ` B ) ) ) |
10 |
7 9
|
opeq12d |
|- ( y = B -> <. ( ( 1st ` A ) .N ( 1st ` y ) ) , ( ( 2nd ` A ) .N ( 2nd ` y ) ) >. = <. ( ( 1st ` A ) .N ( 1st ` B ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) |
11 |
|
df-mpq |
|- .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. ) |
12 |
|
opex |
|- <. ( ( 1st ` A ) .N ( 1st ` B ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. e. _V |
13 |
5 10 11 12
|
ovmpo |
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A .pQ B ) = <. ( ( 1st ` A ) .N ( 1st ` B ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) |