This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mulcomnq

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 mulcomnq 
|- ( A .Q B ) = ( B .Q A )

Proof

Step Hyp Ref Expression
1 mulcompq 
 |-  ( A .pQ B ) = ( B .pQ A )
2 1 fveq2i 
 |-  ( /Q ` ( A .pQ B ) ) = ( /Q ` ( B .pQ A ) )
3 mulpqnq 
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( A .Q B ) = ( /Q ` ( A .pQ B ) ) )
4 mulpqnq 
 |-  ( ( B e. Q. /\ A e. Q. ) -> ( B .Q A ) = ( /Q ` ( B .pQ A ) ) )
5 4 ancoms 
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( B .Q A ) = ( /Q ` ( B .pQ A ) ) )
6 2 3 5 3eqtr4a 
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( A .Q B ) = ( B .Q A ) )
7 mulnqf 
 |-  .Q : ( Q. X. Q. ) --> Q.
8 7 fdmi 
 |-  dom .Q = ( Q. X. Q. )
9 8 ndmovcom 
 |-  ( -. ( A e. Q. /\ B e. Q. ) -> ( A .Q B ) = ( B .Q A ) )
10 6 9 pm2.61i 
 |-  ( A .Q B ) = ( B .Q A )