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

Proof

Step Hyp Ref Expression
1 df-nr ⊢ R = ( ( P × P ) / ~R )
2 mulsrpr ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) = [ ⟨ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) , ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ⟩ ] ~R )
3 mulsrpr ⊢ ( ( ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ∧ ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ) → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ·R [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ) = [ ⟨ ( ( 𝑧 ·P 𝑥 ) +P ( 𝑤 ·P 𝑦 ) ) , ( ( 𝑧 ·P 𝑦 ) +P ( 𝑤 ·P 𝑥 ) ) ⟩ ] ~R )
4 mulcompr ⊢ ( 𝑥 ·P 𝑧 ) = ( 𝑧 ·P 𝑥 )
5 mulcompr ⊢ ( 𝑦 ·P 𝑤 ) = ( 𝑤 ·P 𝑦 )
6 4 5 oveq12i ⊢ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) = ( ( 𝑧 ·P 𝑥 ) +P ( 𝑤 ·P 𝑦 ) )
7 mulcompr ⊢ ( 𝑥 ·P 𝑤 ) = ( 𝑤 ·P 𝑥 )
8 mulcompr ⊢ ( 𝑦 ·P 𝑧 ) = ( 𝑧 ·P 𝑦 )
9 7 8 oveq12i ⊢ ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) = ( ( 𝑤 ·P 𝑥 ) +P ( 𝑧 ·P 𝑦 ) )
10 addcompr ⊢ ( ( 𝑤 ·P 𝑥 ) +P ( 𝑧 ·P 𝑦 ) ) = ( ( 𝑧 ·P 𝑦 ) +P ( 𝑤 ·P 𝑥 ) )
11 9 10 eqtri ⊢ ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) = ( ( 𝑧 ·P 𝑦 ) +P ( 𝑤 ·P 𝑥 ) )
12 1 2 3 6 11 ecovcom ⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( 𝐴 ·R 𝐵 ) = ( 𝐵 ·R 𝐴 ) )
13 dmmulsr ⊢ dom ·R = ( R × R )
14 13 ndmovcom ⊢ ( ¬ ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( 𝐴 ·R 𝐵 ) = ( 𝐵 ·R 𝐴 ) )
15 12 14 pm2.61i ⊢ ( 𝐴 ·R 𝐵 ) = ( 𝐵 ·R 𝐴 )