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 )