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 .R B ) = ( B .R A )

Proof

Step	Hyp	Ref	Expression
1		df-nr	|- R. = ( ( P. X. P. ) /. ~R )
2		mulsrpr	|- ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( [ <. x , y >. ] ~R .R [ <. z , w >. ] ~R ) = [ <. ( ( x .P. z ) +P. ( y .P. w ) ) , ( ( x .P. w ) +P. ( y .P. z ) ) >. ] ~R )
3		mulsrpr	|- ( ( ( z e. P. /\ w e. P. ) /\ ( x e. P. /\ y e. P. ) ) -> ( [ <. z , w >. ] ~R .R [ <. x , y >. ] ~R ) = [ <. ( ( z .P. x ) +P. ( w .P. y ) ) , ( ( z .P. y ) +P. ( w .P. x ) ) >. ] ~R )
4		mulcompr	|- ( x .P. z ) = ( z .P. x )
5		mulcompr	|- ( y .P. w ) = ( w .P. y )
6	4 5	oveq12i	|- ( ( x .P. z ) +P. ( y .P. w ) ) = ( ( z .P. x ) +P. ( w .P. y ) )
7		mulcompr	|- ( x .P. w ) = ( w .P. x )
8		mulcompr	|- ( y .P. z ) = ( z .P. y )
9	7 8	oveq12i	|- ( ( x .P. w ) +P. ( y .P. z ) ) = ( ( w .P. x ) +P. ( z .P. y ) )
10		addcompr	|- ( ( w .P. x ) +P. ( z .P. y ) ) = ( ( z .P. y ) +P. ( w .P. x ) )
11	9 10	eqtri	|- ( ( x .P. w ) +P. ( y .P. z ) ) = ( ( z .P. y ) +P. ( w .P. x ) )
12	1 2 3 6 11	ecovcom	|- ( ( A e. R. /\ B e. R. ) -> ( A .R B ) = ( B .R A ) )
13		dmmulsr	|- dom .R = ( R. X. R. )
14	13	ndmovcom	|- ( -. ( A e. R. /\ B e. R. ) -> ( A .R B ) = ( B .R A ) )
15	12 14	pm2.61i	|- ( A .R B ) = ( B .R A )