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{\cdot }_{\mathrm{𝑝𝑸}}B=B{\cdot }_{\mathrm{𝑝𝑸}}A$$

Proof

Step	Hyp	Ref	Expression
1		mulcompi	$$⊢1^{st}\left(A\right){\cdot }_{𝑵}{1}^{st}\left(B\right)=1^{st}\left(B\right){\cdot }_{𝑵}{1}^{st}\left(A\right)$$
2		mulcompi	$$⊢2^{nd}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)=2^{nd}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)$$
3	1 2	opeq12i	$$⊢⟨1^{st}\left(A\right){\cdot }_{𝑵}{1}^{st}\left(B\right),2^{nd}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)⟩=⟨1^{st}\left(B\right){\cdot }_{𝑵}{1}^{st}\left(A\right),2^{nd}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)⟩$$
4		mulpipq2	$$⊢\left(A\in \left(𝑵\times 𝑵\right)\wedge B\in \left(𝑵\times 𝑵\right)\right)\to A{\cdot }_{\mathrm{𝑝𝑸}}B=⟨1^{st}\left(A\right){\cdot }_{𝑵}{1}^{st}\left(B\right),2^{nd}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)⟩$$
5		mulpipq2	$$⊢\left(B\in \left(𝑵\times 𝑵\right)\wedge A\in \left(𝑵\times 𝑵\right)\right)\to B{\cdot }_{\mathrm{𝑝𝑸}}A=⟨1^{st}\left(B\right){\cdot }_{𝑵}{1}^{st}\left(A\right),2^{nd}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)⟩$$
6	5	ancoms	$$⊢\left(A\in \left(𝑵\times 𝑵\right)\wedge B\in \left(𝑵\times 𝑵\right)\right)\to B{\cdot }_{\mathrm{𝑝𝑸}}A=⟨1^{st}\left(B\right){\cdot }_{𝑵}{1}^{st}\left(A\right),2^{nd}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)⟩$$
7	3 4 6	3eqtr4a	$$⊢\left(A\in \left(𝑵\times 𝑵\right)\wedge B\in \left(𝑵\times 𝑵\right)\right)\to A{\cdot }_{\mathrm{𝑝𝑸}}B=B{\cdot }_{\mathrm{𝑝𝑸}}A$$
8		mulpqf	$$⊢{\cdot }_{\mathrm{𝑝𝑸}}:\left(𝑵\times 𝑵\right)\times \left(𝑵\times 𝑵\right)⟶𝑵\times 𝑵$$
9	8	fdmi	$$⊢\mathrm{dom}{\cdot }_{\mathrm{𝑝𝑸}}=\left(𝑵\times 𝑵\right)\times \left(𝑵\times 𝑵\right)$$
10	9	ndmovcom	$$⊢\neg \left(A\in \left(𝑵\times 𝑵\right)\wedge B\in \left(𝑵\times 𝑵\right)\right)\to A{\cdot }_{\mathrm{𝑝𝑸}}B=B{\cdot }_{\mathrm{𝑝𝑸}}A$$
11	7 10	pm2.61i	$$⊢A{\cdot }_{\mathrm{𝑝𝑸}}B=B{\cdot }_{\mathrm{𝑝𝑸}}A$$