Metamath Proof Explorer

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

Proof

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