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{\cdot }_{𝑹}B=B{\cdot }_{𝑹}A$$

Proof

Step	Hyp	Ref	Expression
1		df-nr	$$⊢𝑹=\left(𝑷\times 𝑷\right)/{~}_{𝑹}$$
2		mulsrpr	$$⊢\left(\left(x\in 𝑷\wedge y\in 𝑷\right)\wedge \left(z\in 𝑷\wedge w\in 𝑷\right)\right)\to \left[⟨x,y⟩\right]{~}_{𝑹}{\cdot }_{𝑹}\left[⟨z,w⟩\right]{~}_{𝑹}=\left[⟨\left(x{\cdot }_{𝑷}z\right){+}_{𝑷}\left(y{\cdot }_{𝑷}w\right),\left(x{\cdot }_{𝑷}w\right){+}_{𝑷}\left(y{\cdot }_{𝑷}z\right)⟩\right]{~}_{𝑹}$$
3		mulsrpr	$$⊢\left(\left(z\in 𝑷\wedge w\in 𝑷\right)\wedge \left(x\in 𝑷\wedge y\in 𝑷\right)\right)\to \left[⟨z,w⟩\right]{~}_{𝑹}{\cdot }_{𝑹}\left[⟨x,y⟩\right]{~}_{𝑹}=\left[⟨\left(z{\cdot }_{𝑷}x\right){+}_{𝑷}\left(w{\cdot }_{𝑷}y\right),\left(z{\cdot }_{𝑷}y\right){+}_{𝑷}\left(w{\cdot }_{𝑷}x\right)⟩\right]{~}_{𝑹}$$
4		mulcompr	$$⊢x{\cdot }_{𝑷}z=z{\cdot }_{𝑷}x$$
5		mulcompr	$$⊢y{\cdot }_{𝑷}w=w{\cdot }_{𝑷}y$$
6	4 5	oveq12i	$$⊢\left(x{\cdot }_{𝑷}z\right){+}_{𝑷}\left(y{\cdot }_{𝑷}w\right)=\left(z{\cdot }_{𝑷}x\right){+}_{𝑷}\left(w{\cdot }_{𝑷}y\right)$$
7		mulcompr	$$⊢x{\cdot }_{𝑷}w=w{\cdot }_{𝑷}x$$
8		mulcompr	$$⊢y{\cdot }_{𝑷}z=z{\cdot }_{𝑷}y$$
9	7 8	oveq12i	$$⊢\left(x{\cdot }_{𝑷}w\right){+}_{𝑷}\left(y{\cdot }_{𝑷}z\right)=\left(w{\cdot }_{𝑷}x\right){+}_{𝑷}\left(z{\cdot }_{𝑷}y\right)$$
10		addcompr	$$⊢\left(w{\cdot }_{𝑷}x\right){+}_{𝑷}\left(z{\cdot }_{𝑷}y\right)=\left(z{\cdot }_{𝑷}y\right){+}_{𝑷}\left(w{\cdot }_{𝑷}x\right)$$
11	9 10	eqtri	$$⊢\left(x{\cdot }_{𝑷}w\right){+}_{𝑷}\left(y{\cdot }_{𝑷}z\right)=\left(z{\cdot }_{𝑷}y\right){+}_{𝑷}\left(w{\cdot }_{𝑷}x\right)$$
12	1 2 3 6 11	ecovcom	$$⊢\left(A\in 𝑹\wedge B\in 𝑹\right)\to A{\cdot }_{𝑹}B=B{\cdot }_{𝑹}A$$
13		dmmulsr	$$⊢\mathrm{dom}{\cdot }_{𝑹}=𝑹\times 𝑹$$
14	13	ndmovcom	$$⊢\neg \left(A\in 𝑹\wedge B\in 𝑹\right)\to A{\cdot }_{𝑹}B=B{\cdot }_{𝑹}A$$
15	12 14	pm2.61i	$$⊢A{\cdot }_{𝑹}B=B{\cdot }_{𝑹}A$$