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