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 𝐴 )