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	⊢ ( 𝐴 ·Q 𝐵 ) = ( 𝐵 ·Q 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		mulcompq	⊢ ( 𝐴 ·pQ 𝐵 ) = ( 𝐵 ·pQ 𝐴 )
2	1	fveq2i	⊢ ( [Q] ‘ ( 𝐴 ·pQ 𝐵 ) ) = ( [Q] ‘ ( 𝐵 ·pQ 𝐴 ) )
3		mulpqnq	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( 𝐴 ·Q 𝐵 ) = ( [Q] ‘ ( 𝐴 ·pQ 𝐵 ) ) )
4		mulpqnq	⊢ ( ( 𝐵 ∈ Q ∧ 𝐴 ∈ Q ) → ( 𝐵 ·Q 𝐴 ) = ( [Q] ‘ ( 𝐵 ·pQ 𝐴 ) ) )
5	4	ancoms	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( 𝐵 ·Q 𝐴 ) = ( [Q] ‘ ( 𝐵 ·pQ 𝐴 ) ) )
6	2 3 5	3eqtr4a	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( 𝐴 ·Q 𝐵 ) = ( 𝐵 ·Q 𝐴 ) )
7		mulnqf	⊢ ·Q : ( Q × Q ) ⟶ Q
8	7	fdmi	⊢ dom ·Q = ( Q × Q )
9	8	ndmovcom	⊢ ( ¬ ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( 𝐴 ·Q 𝐵 ) = ( 𝐵 ·Q 𝐴 ) )
10	6 9	pm2.61i	⊢ ( 𝐴 ·Q 𝐵 ) = ( 𝐵 ·Q 𝐴 )