Metamath Proof Explorer

Theorem addcomsr

Description: Addition 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 addcomsr 
|- ( A +R B ) = ( B +R A )

Proof

Step Hyp Ref Expression
1 df-nr 
 |-  R. = ( ( P. X. P. ) /. ~R )
2 addsrpr 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( [ <. x , y >. ] ~R +R [ <. z , w >. ] ~R ) = [ <. ( x +P. z ) , ( y +P. w ) >. ] ~R )
3 addsrpr 
 |-  ( ( ( z e. P. /\ w e. P. ) /\ ( x e. P. /\ y e. P. ) ) -> ( [ <. z , w >. ] ~R +R [ <. x , y >. ] ~R ) = [ <. ( z +P. x ) , ( w +P. y ) >. ] ~R )
4 addcompr 
 |-  ( x +P. z ) = ( z +P. x )
5 addcompr 
 |-  ( y +P. w ) = ( w +P. y )
6 1 2 3 4 5 ecovcom 
 |-  ( ( A e. R. /\ B e. R. ) -> ( A +R B ) = ( B +R A ) )
7 dmaddsr 
 |-  dom +R = ( R. X. R. )
8 7 ndmovcom 
 |-  ( -. ( A e. R. /\ B e. R. ) -> ( A +R B ) = ( B +R A ) )
9 6 8 pm2.61i 
 |-  ( A +R B ) = ( B +R A )