This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⋅ 𝑝𝑸 B = B ⋅ 𝑝𝑸 A

Proof

Step Hyp Ref Expression
1 mulcompi ⊢ 1 st ⁡ A ⋅ 𝑵 1 st ⁡ B = 1 st ⁡ B ⋅ 𝑵 1 st ⁡ A
2 mulcompi ⊢ 2 nd ⁡ A ⋅ 𝑵 2 nd ⁡ B = 2 nd ⁡ B ⋅ 𝑵 2 nd ⁡ A
3 1 2 opeq12i ⊢ 1 st ⁡ A ⋅ 𝑵 1 st ⁡ B 2 nd ⁡ A ⋅ 𝑵 2 nd ⁡ B = 1 st ⁡ B ⋅ 𝑵 1 st ⁡ A 2 nd ⁡ B ⋅ 𝑵 2 nd ⁡ A
4 mulpipq2 ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 → A ⋅ 𝑝𝑸 B = 1 st ⁡ A ⋅ 𝑵 1 st ⁡ B 2 nd ⁡ A ⋅ 𝑵 2 nd ⁡ B
5 mulpipq2 ⊢ B ∈ 𝑵 × 𝑵 ∧ A ∈ 𝑵 × 𝑵 → B ⋅ 𝑝𝑸 A = 1 st ⁡ B ⋅ 𝑵 1 st ⁡ A 2 nd ⁡ B ⋅ 𝑵 2 nd ⁡ A
6 5 ancoms ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 → B ⋅ 𝑝𝑸 A = 1 st ⁡ B ⋅ 𝑵 1 st ⁡ A 2 nd ⁡ B ⋅ 𝑵 2 nd ⁡ A
7 3 4 6 3eqtr4a ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 → A ⋅ 𝑝𝑸 B = B ⋅ 𝑝𝑸 A
8 mulpqf ⊢ ⋅ 𝑝𝑸 : 𝑵 × 𝑵 × 𝑵 × 𝑵 ⟶ 𝑵 × 𝑵
9 8 fdmi ⊢ dom ⁡ ⋅ 𝑝𝑸 = 𝑵 × 𝑵 × 𝑵 × 𝑵
10 9 ndmovcom ⊢ ¬ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 → A ⋅ 𝑝𝑸 B = B ⋅ 𝑝𝑸 A
11 7 10 pm2.61i ⊢ A ⋅ 𝑝𝑸 B = B ⋅ 𝑝𝑸 A