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

Metamath Proof Explorer

Theorem mulcomsr

Description: Multiplication of signed reals is commutative. (Contributed by NM, 31-Aug-1995) (Revised by Mario Carneiro, 28-Apr-2015) (New usage is discouraged.)

Ref Expression
Assertion mulcomsr ⊢ A ⋅ 𝑹 B = B ⋅ 𝑹 A

Proof

Step Hyp Ref Expression
1 df-nr ⊢ 𝑹 = 𝑷 × 𝑷 / ~ 𝑹
2 mulsrpr ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 ∧ z ∈ 𝑷 ∧ w ∈ 𝑷 → x y ~ 𝑹 ⋅ 𝑹 z w ~ 𝑹 = x ⋅ 𝑷 z + 𝑷 y ⋅ 𝑷 w x ⋅ 𝑷 w + 𝑷 y ⋅ 𝑷 z ~ 𝑹
3 mulsrpr ⊢ z ∈ 𝑷 ∧ w ∈ 𝑷 ∧ x ∈ 𝑷 ∧ y ∈ 𝑷 → z w ~ 𝑹 ⋅ 𝑹 x y ~ 𝑹 = z ⋅ 𝑷 x + 𝑷 w ⋅ 𝑷 y z ⋅ 𝑷 y + 𝑷 w ⋅ 𝑷 x ~ 𝑹
4 mulcompr ⊢ x ⋅ 𝑷 z = z ⋅ 𝑷 x
5 mulcompr ⊢ y ⋅ 𝑷 w = w ⋅ 𝑷 y
6 4 5 oveq12i ⊢ x ⋅ 𝑷 z + 𝑷 y ⋅ 𝑷 w = z ⋅ 𝑷 x + 𝑷 w ⋅ 𝑷 y
7 mulcompr ⊢ x ⋅ 𝑷 w = w ⋅ 𝑷 x
8 mulcompr ⊢ y ⋅ 𝑷 z = z ⋅ 𝑷 y
9 7 8 oveq12i ⊢ x ⋅ 𝑷 w + 𝑷 y ⋅ 𝑷 z = w ⋅ 𝑷 x + 𝑷 z ⋅ 𝑷 y
10 addcompr ⊢ w ⋅ 𝑷 x + 𝑷 z ⋅ 𝑷 y = z ⋅ 𝑷 y + 𝑷 w ⋅ 𝑷 x
11 9 10 eqtri ⊢ x ⋅ 𝑷 w + 𝑷 y ⋅ 𝑷 z = z ⋅ 𝑷 y + 𝑷 w ⋅ 𝑷 x
12 1 2 3 6 11 ecovcom ⊢ A ∈ 𝑹 ∧ B ∈ 𝑹 → A ⋅ 𝑹 B = B ⋅ 𝑹 A
13 dmmulsr ⊢ dom ⁡ ⋅ 𝑹 = 𝑹 × 𝑹
14 13 ndmovcom ⊢ ¬ A ∈ 𝑹 ∧ B ∈ 𝑹 → A ⋅ 𝑹 B = B ⋅ 𝑹 A
15 12 14 pm2.61i ⊢ A ⋅ 𝑹 B = B ⋅ 𝑹 A