Metamath Proof Explorer

Theorem addasssr

Description: Addition of signed reals is associative. (Contributed by NM, 2-Sep-1995) (Revised by Mario Carneiro, 28-Apr-2015) (New usage is discouraged.)

Ref Expression
Assertion addasssr 
|- ( ( A +R B ) +R C ) = ( A +R ( B +R C ) )

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. ) /\ ( v e. P. /\ u e. P. ) ) -> ( [ <. z , w >. ] ~R +R [ <. v , u >. ] ~R ) = [ <. ( z +P. v ) , ( w +P. u ) >. ] ~R )
4 addsrpr 
 |-  ( ( ( ( x +P. z ) e. P. /\ ( y +P. w ) e. P. ) /\ ( v e. P. /\ u e. P. ) ) -> ( [ <. ( x +P. z ) , ( y +P. w ) >. ] ~R +R [ <. v , u >. ] ~R ) = [ <. ( ( x +P. z ) +P. v ) , ( ( y +P. w ) +P. u ) >. ] ~R )
5 addsrpr 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( ( z +P. v ) e. P. /\ ( w +P. u ) e. P. ) ) -> ( [ <. x , y >. ] ~R +R [ <. ( z +P. v ) , ( w +P. u ) >. ] ~R ) = [ <. ( x +P. ( z +P. v ) ) , ( y +P. ( w +P. u ) ) >. ] ~R )
6 addclpr 
 |-  ( ( x e. P. /\ z e. P. ) -> ( x +P. z ) e. P. )
7 addclpr 
 |-  ( ( y e. P. /\ w e. P. ) -> ( y +P. w ) e. P. )
8 6 7 anim12i 
 |-  ( ( ( x e. P. /\ z e. P. ) /\ ( y e. P. /\ w e. P. ) ) -> ( ( x +P. z ) e. P. /\ ( y +P. w ) e. P. ) )
9 8 an4s 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( ( x +P. z ) e. P. /\ ( y +P. w ) e. P. ) )
10 addclpr 
 |-  ( ( z e. P. /\ v e. P. ) -> ( z +P. v ) e. P. )
11 addclpr 
 |-  ( ( w e. P. /\ u e. P. ) -> ( w +P. u ) e. P. )
12 10 11 anim12i 
 |-  ( ( ( z e. P. /\ v e. P. ) /\ ( w e. P. /\ u e. P. ) ) -> ( ( z +P. v ) e. P. /\ ( w +P. u ) e. P. ) )
13 12 an4s 
 |-  ( ( ( z e. P. /\ w e. P. ) /\ ( v e. P. /\ u e. P. ) ) -> ( ( z +P. v ) e. P. /\ ( w +P. u ) e. P. ) )
14 addasspr 
 |-  ( ( x +P. z ) +P. v ) = ( x +P. ( z +P. v ) )
15 addasspr 
 |-  ( ( y +P. w ) +P. u ) = ( y +P. ( w +P. u ) )
16 1 2 3 4 5 9 13 14 15 ecovass 
 |-  ( ( A e. R. /\ B e. R. /\ C e. R. ) -> ( ( A +R B ) +R C ) = ( A +R ( B +R C ) ) )
17 dmaddsr 
 |-  dom +R = ( R. X. R. )
18 0nsr 
 |-  -. (/) e. R.
19 17 18 ndmovass 
 |-  ( -. ( A e. R. /\ B e. R. /\ C e. R. ) -> ( ( A +R B ) +R C ) = ( A +R ( B +R C ) ) )
20 16 19 pm2.61i 
 |-  ( ( A +R B ) +R C ) = ( A +R ( B +R C ) )