Metamath Proof Explorer

Theorem mulcompq

Description: Multiplication of positive fractions is commutative. (Contributed by NM, 31-Aug-1995) (Revised by Mario Carneiro, 28-Apr-2013) (New usage is discouraged.)

Ref Expression
Assertion mulcompq 
|- ( A .pQ B ) = ( B .pQ A )

Proof

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 )