Metamath Proof Explorer

Theorem mulasssr

Description: Multiplication 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 mulasssr 
|- ( ( A .R B ) .R C ) = ( A .R ( B .R C ) )

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. ) /\ ( v e. P. /\ u e. P. ) ) -> ( [ <. z , w >. ] ~R .R [ <. v , u >. ] ~R ) = [ <. ( ( z .P. v ) +P. ( w .P. u ) ) , ( ( z .P. u ) +P. ( w .P. v ) ) >. ] ~R )
4 mulsrpr 
 |-  ( ( ( ( ( x .P. z ) +P. ( y .P. w ) ) e. P. /\ ( ( x .P. w ) +P. ( y .P. z ) ) e. P. ) /\ ( v e. P. /\ u e. P. ) ) -> ( [ <. ( ( x .P. z ) +P. ( y .P. w ) ) , ( ( x .P. w ) +P. ( y .P. z ) ) >. ] ~R .R [ <. v , u >. ] ~R ) = [ <. ( ( ( ( x .P. z ) +P. ( y .P. w ) ) .P. v ) +P. ( ( ( x .P. w ) +P. ( y .P. z ) ) .P. u ) ) , ( ( ( ( x .P. z ) +P. ( y .P. w ) ) .P. u ) +P. ( ( ( x .P. w ) +P. ( y .P. z ) ) .P. v ) ) >. ] ~R )
5 mulsrpr 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( ( ( z .P. v ) +P. ( w .P. u ) ) e. P. /\ ( ( z .P. u ) +P. ( w .P. v ) ) e. P. ) ) -> ( [ <. x , y >. ] ~R .R [ <. ( ( z .P. v ) +P. ( w .P. u ) ) , ( ( z .P. u ) +P. ( w .P. v ) ) >. ] ~R ) = [ <. ( ( x .P. ( ( z .P. v ) +P. ( w .P. u ) ) ) +P. ( y .P. ( ( z .P. u ) +P. ( w .P. v ) ) ) ) , ( ( x .P. ( ( z .P. u ) +P. ( w .P. v ) ) ) +P. ( y .P. ( ( z .P. v ) +P. ( w .P. u ) ) ) ) >. ] ~R )
6 mulclpr 
 |-  ( ( x e. P. /\ z e. P. ) -> ( x .P. z ) e. P. )
7 mulclpr 
 |-  ( ( y e. P. /\ w e. P. ) -> ( y .P. w ) e. P. )
8 addclpr 
 |-  ( ( ( x .P. z ) e. P. /\ ( y .P. w ) e. P. ) -> ( ( x .P. z ) +P. ( y .P. w ) ) e. P. )
9 6 7 8 syl2an 
 |-  ( ( ( x e. P. /\ z e. P. ) /\ ( y e. P. /\ w e. P. ) ) -> ( ( x .P. z ) +P. ( y .P. w ) ) e. P. )
10 9 an4s 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( ( x .P. z ) +P. ( y .P. w ) ) e. P. )
11 mulclpr 
 |-  ( ( x e. P. /\ w e. P. ) -> ( x .P. w ) e. P. )
12 mulclpr 
 |-  ( ( y e. P. /\ z e. P. ) -> ( y .P. z ) e. P. )
13 addclpr 
 |-  ( ( ( x .P. w ) e. P. /\ ( y .P. z ) e. P. ) -> ( ( x .P. w ) +P. ( y .P. z ) ) e. P. )
14 11 12 13 syl2an 
 |-  ( ( ( x e. P. /\ w e. P. ) /\ ( y e. P. /\ z e. P. ) ) -> ( ( x .P. w ) +P. ( y .P. z ) ) e. P. )
15 14 an42s 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( ( x .P. w ) +P. ( y .P. z ) ) e. P. )
16 10 15 jca 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( ( ( x .P. z ) +P. ( y .P. w ) ) e. P. /\ ( ( x .P. w ) +P. ( y .P. z ) ) e. P. ) )
17 mulclpr 
 |-  ( ( z e. P. /\ v e. P. ) -> ( z .P. v ) e. P. )
18 mulclpr 
 |-  ( ( w e. P. /\ u e. P. ) -> ( w .P. u ) e. P. )
19 addclpr 
 |-  ( ( ( z .P. v ) e. P. /\ ( w .P. u ) e. P. ) -> ( ( z .P. v ) +P. ( w .P. u ) ) e. P. )
20 17 18 19 syl2an 
 |-  ( ( ( z e. P. /\ v e. P. ) /\ ( w e. P. /\ u e. P. ) ) -> ( ( z .P. v ) +P. ( w .P. u ) ) e. P. )
21 20 an4s 
 |-  ( ( ( z e. P. /\ w e. P. ) /\ ( v e. P. /\ u e. P. ) ) -> ( ( z .P. v ) +P. ( w .P. u ) ) e. P. )
22 mulclpr 
 |-  ( ( z e. P. /\ u e. P. ) -> ( z .P. u ) e. P. )
23 mulclpr 
 |-  ( ( w e. P. /\ v e. P. ) -> ( w .P. v ) e. P. )
24 addclpr 
 |-  ( ( ( z .P. u ) e. P. /\ ( w .P. v ) e. P. ) -> ( ( z .P. u ) +P. ( w .P. v ) ) e. P. )
25 22 23 24 syl2an 
 |-  ( ( ( z e. P. /\ u e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( ( z .P. u ) +P. ( w .P. v ) ) e. P. )
26 25 an42s 
 |-  ( ( ( z e. P. /\ w e. P. ) /\ ( v e. P. /\ u e. P. ) ) -> ( ( z .P. u ) +P. ( w .P. v ) ) e. P. )
27 21 26 jca 
 |-  ( ( ( z e. P. /\ w e. P. ) /\ ( v e. P. /\ u e. P. ) ) -> ( ( ( z .P. v ) +P. ( w .P. u ) ) e. P. /\ ( ( z .P. u ) +P. ( w .P. v ) ) e. P. ) )
28 vex 
 |-  x e. _V
29 vex 
 |-  y e. _V
30 vex 
 |-  z e. _V
31 mulcompr 
 |-  ( f .P. g ) = ( g .P. f )
32 distrpr 
 |-  ( f .P. ( g +P. h ) ) = ( ( f .P. g ) +P. ( f .P. h ) )
33 vex 
 |-  w e. _V
34 vex 
 |-  v e. _V
35 mulasspr 
 |-  ( ( f .P. g ) .P. h ) = ( f .P. ( g .P. h ) )
36 vex 
 |-  u e. _V
37 addcompr 
 |-  ( f +P. g ) = ( g +P. f )
38 addasspr 
 |-  ( ( f +P. g ) +P. h ) = ( f +P. ( g +P. h ) )
39 28 29 30 31 32 33 34 35 36 37 38 caovlem2 
 |-  ( ( ( ( x .P. z ) +P. ( y .P. w ) ) .P. v ) +P. ( ( ( x .P. w ) +P. ( y .P. z ) ) .P. u ) ) = ( ( x .P. ( ( z .P. v ) +P. ( w .P. u ) ) ) +P. ( y .P. ( ( z .P. u ) +P. ( w .P. v ) ) ) )
40 28 29 30 31 32 33 36 35 34 37 38 caovlem2 
 |-  ( ( ( ( x .P. z ) +P. ( y .P. w ) ) .P. u ) +P. ( ( ( x .P. w ) +P. ( y .P. z ) ) .P. v ) ) = ( ( x .P. ( ( z .P. u ) +P. ( w .P. v ) ) ) +P. ( y .P. ( ( z .P. v ) +P. ( w .P. u ) ) ) )
41 1 2 3 4 5 16 27 39 40 ecovass 
 |-  ( ( A e. R. /\ B e. R. /\ C e. R. ) -> ( ( A .R B ) .R C ) = ( A .R ( B .R C ) ) )
42 dmmulsr 
 |-  dom .R = ( R. X. R. )
43 0nsr 
 |-  -. (/) e. R.
44 42 43 ndmovass 
 |-  ( -. ( A e. R. /\ B e. R. /\ C e. R. ) -> ( ( A .R B ) .R C ) = ( A .R ( B .R C ) ) )
45 41 44 pm2.61i 
 |-  ( ( A .R B ) .R C ) = ( A .R ( B .R C ) )