Step |
Hyp |
Ref |
Expression |
1 |
|
mulcompi |
|- ( ( 1st ` A ) .N ( 1st ` B ) ) = ( ( 1st ` B ) .N ( 1st ` A ) ) |
2 |
|
mulcompi |
|- ( ( 2nd ` A ) .N ( 2nd ` B ) ) = ( ( 2nd ` B ) .N ( 2nd ` A ) ) |
3 |
1 2
|
opeq12i |
|- <. ( ( 1st ` A ) .N ( 1st ` B ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. = <. ( ( 1st ` B ) .N ( 1st ` A ) ) , ( ( 2nd ` B ) .N ( 2nd ` A ) ) >. |
4 |
|
mulpipq2 |
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A .pQ B ) = <. ( ( 1st ` A ) .N ( 1st ` B ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) |
5 |
|
mulpipq2 |
|- ( ( B e. ( N. X. N. ) /\ A e. ( N. X. N. ) ) -> ( B .pQ A ) = <. ( ( 1st ` B ) .N ( 1st ` A ) ) , ( ( 2nd ` B ) .N ( 2nd ` A ) ) >. ) |
6 |
5
|
ancoms |
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( B .pQ A ) = <. ( ( 1st ` B ) .N ( 1st ` A ) ) , ( ( 2nd ` B ) .N ( 2nd ` A ) ) >. ) |
7 |
3 4 6
|
3eqtr4a |
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A .pQ B ) = ( B .pQ A ) ) |
8 |
|
mulpqf |
|- .pQ : ( ( N. X. N. ) X. ( N. X. N. ) ) --> ( N. X. N. ) |
9 |
8
|
fdmi |
|- dom .pQ = ( ( N. X. N. ) X. ( N. X. N. ) ) |
10 |
9
|
ndmovcom |
|- ( -. ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A .pQ B ) = ( B .pQ A ) ) |
11 |
7 10
|
pm2.61i |
|- ( A .pQ B ) = ( B .pQ A ) |