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 ( 𝐴 ·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 𝐴 )