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