Metamath Proof Explorer

Theorem distrsr

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

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

Proof

Step Hyp Ref Expression
1 df-nr 
 |-  R. = ( ( P. X. P. ) /. ~R )
2 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 )
3 mulsrpr 
 |-  ( ( ( 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 ) ) +P. ( y .P. ( w +P. u ) ) ) , ( ( x .P. ( w +P. u ) ) +P. ( y .P. ( z +P. v ) ) ) >. ] ~R )
4 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 )
5 mulsrpr 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( v e. P. /\ u e. P. ) ) -> ( [ <. x , y >. ] ~R .R [ <. v , u >. ] ~R ) = [ <. ( ( x .P. v ) +P. ( y .P. u ) ) , ( ( x .P. u ) +P. ( y .P. v ) ) >. ] ~R )
6 addsrpr 
 |-  ( ( ( ( ( x .P. z ) +P. ( y .P. w ) ) e. P. /\ ( ( x .P. w ) +P. ( y .P. z ) ) e. P. ) /\ ( ( ( x .P. v ) +P. ( y .P. u ) ) e. P. /\ ( ( x .P. u ) +P. ( y .P. v ) ) e. P. ) ) -> ( [ <. ( ( x .P. z ) +P. ( y .P. w ) ) , ( ( x .P. w ) +P. ( y .P. z ) ) >. ] ~R +R [ <. ( ( x .P. v ) +P. ( y .P. u ) ) , ( ( x .P. u ) +P. ( y .P. v ) ) >. ] ~R ) = [ <. ( ( ( x .P. z ) +P. ( y .P. w ) ) +P. ( ( x .P. v ) +P. ( y .P. u ) ) ) , ( ( ( x .P. w ) +P. ( y .P. z ) ) +P. ( ( x .P. u ) +P. ( y .P. v ) ) ) >. ] ~R )
7 addclpr 
 |-  ( ( z e. P. /\ v e. P. ) -> ( z +P. v ) e. P. )
8 addclpr 
 |-  ( ( w e. P. /\ u e. P. ) -> ( w +P. u ) e. P. )
9 7 8 anim12i 
 |-  ( ( ( z e. P. /\ v e. P. ) /\ ( w e. P. /\ u e. P. ) ) -> ( ( z +P. v ) e. P. /\ ( w +P. u ) e. P. ) )
10 9 an4s 
 |-  ( ( ( z e. P. /\ w e. P. ) /\ ( v e. P. /\ u e. P. ) ) -> ( ( z +P. v ) e. P. /\ ( w +P. u ) e. P. ) )
11 mulclpr 
 |-  ( ( x e. P. /\ z e. P. ) -> ( x .P. z ) e. P. )
12 mulclpr 
 |-  ( ( y e. P. /\ w e. P. ) -> ( y .P. w ) e. P. )
13 addclpr 
 |-  ( ( ( x .P. z ) e. P. /\ ( y .P. w ) e. P. ) -> ( ( x .P. z ) +P. ( y .P. w ) ) e. P. )
14 11 12 13 syl2an 
 |-  ( ( ( x e. P. /\ z e. P. ) /\ ( y e. P. /\ w e. P. ) ) -> ( ( x .P. z ) +P. ( y .P. w ) ) e. P. )
15 14 an4s 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( ( x .P. z ) +P. ( y .P. w ) ) e. P. )
16 mulclpr 
 |-  ( ( x e. P. /\ w e. P. ) -> ( x .P. w ) e. P. )
17 mulclpr 
 |-  ( ( y e. P. /\ z e. P. ) -> ( y .P. z ) e. P. )
18 addclpr 
 |-  ( ( ( x .P. w ) e. P. /\ ( y .P. z ) e. P. ) -> ( ( x .P. w ) +P. ( y .P. z ) ) e. P. )
19 16 17 18 syl2an 
 |-  ( ( ( x e. P. /\ w e. P. ) /\ ( y e. P. /\ z e. P. ) ) -> ( ( x .P. w ) +P. ( y .P. z ) ) e. P. )
20 19 an42s 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( ( x .P. w ) +P. ( y .P. z ) ) e. P. )
21 15 20 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. ) )
22 mulclpr 
 |-  ( ( x e. P. /\ v e. P. ) -> ( x .P. v ) e. P. )
23 mulclpr 
 |-  ( ( y e. P. /\ u e. P. ) -> ( y .P. u ) e. P. )
24 addclpr 
 |-  ( ( ( x .P. v ) e. P. /\ ( y .P. u ) e. P. ) -> ( ( x .P. v ) +P. ( y .P. u ) ) e. P. )
25 22 23 24 syl2an 
 |-  ( ( ( x e. P. /\ v e. P. ) /\ ( y e. P. /\ u e. P. ) ) -> ( ( x .P. v ) +P. ( y .P. u ) ) e. P. )
26 25 an4s 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( v e. P. /\ u e. P. ) ) -> ( ( x .P. v ) +P. ( y .P. u ) ) e. P. )
27 mulclpr 
 |-  ( ( x e. P. /\ u e. P. ) -> ( x .P. u ) e. P. )
28 mulclpr 
 |-  ( ( y e. P. /\ v e. P. ) -> ( y .P. v ) e. P. )
29 addclpr 
 |-  ( ( ( x .P. u ) e. P. /\ ( y .P. v ) e. P. ) -> ( ( x .P. u ) +P. ( y .P. v ) ) e. P. )
30 27 28 29 syl2an 
 |-  ( ( ( x e. P. /\ u e. P. ) /\ ( y e. P. /\ v e. P. ) ) -> ( ( x .P. u ) +P. ( y .P. v ) ) e. P. )
31 30 an42s 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( v e. P. /\ u e. P. ) ) -> ( ( x .P. u ) +P. ( y .P. v ) ) e. P. )
32 26 31 jca 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( v e. P. /\ u e. P. ) ) -> ( ( ( x .P. v ) +P. ( y .P. u ) ) e. P. /\ ( ( x .P. u ) +P. ( y .P. v ) ) e. P. ) )
33 distrpr 
 |-  ( x .P. ( z +P. v ) ) = ( ( x .P. z ) +P. ( x .P. v ) )
34 distrpr 
 |-  ( y .P. ( w +P. u ) ) = ( ( y .P. w ) +P. ( y .P. u ) )
35 33 34 oveq12i 
 |-  ( ( x .P. ( z +P. v ) ) +P. ( y .P. ( w +P. u ) ) ) = ( ( ( x .P. z ) +P. ( x .P. v ) ) +P. ( ( y .P. w ) +P. ( y .P. u ) ) )
36 ovex 
 |-  ( x .P. z ) e. _V
37 ovex 
 |-  ( x .P. v ) e. _V
38 ovex 
 |-  ( y .P. w ) e. _V
39 addcompr 
 |-  ( f +P. g ) = ( g +P. f )
40 addasspr 
 |-  ( ( f +P. g ) +P. h ) = ( f +P. ( g +P. h ) )
41 ovex 
 |-  ( y .P. u ) e. _V
42 36 37 38 39 40 41 caov4 
 |-  ( ( ( x .P. z ) +P. ( x .P. v ) ) +P. ( ( y .P. w ) +P. ( y .P. u ) ) ) = ( ( ( x .P. z ) +P. ( y .P. w ) ) +P. ( ( x .P. v ) +P. ( y .P. u ) ) )
43 35 42 eqtri 
 |-  ( ( x .P. ( z +P. v ) ) +P. ( y .P. ( w +P. u ) ) ) = ( ( ( x .P. z ) +P. ( y .P. w ) ) +P. ( ( x .P. v ) +P. ( y .P. u ) ) )
44 distrpr 
 |-  ( x .P. ( w +P. u ) ) = ( ( x .P. w ) +P. ( x .P. u ) )
45 distrpr 
 |-  ( y .P. ( z +P. v ) ) = ( ( y .P. z ) +P. ( y .P. v ) )
46 44 45 oveq12i 
 |-  ( ( x .P. ( w +P. u ) ) +P. ( y .P. ( z +P. v ) ) ) = ( ( ( x .P. w ) +P. ( x .P. u ) ) +P. ( ( y .P. z ) +P. ( y .P. v ) ) )
47 ovex 
 |-  ( x .P. w ) e. _V
48 ovex 
 |-  ( x .P. u ) e. _V
49 ovex 
 |-  ( y .P. z ) e. _V
50 ovex 
 |-  ( y .P. v ) e. _V
51 47 48 49 39 40 50 caov4 
 |-  ( ( ( x .P. w ) +P. ( x .P. u ) ) +P. ( ( y .P. z ) +P. ( y .P. v ) ) ) = ( ( ( x .P. w ) +P. ( y .P. z ) ) +P. ( ( x .P. u ) +P. ( y .P. v ) ) )
52 46 51 eqtri 
 |-  ( ( x .P. ( w +P. u ) ) +P. ( y .P. ( z +P. v ) ) ) = ( ( ( x .P. w ) +P. ( y .P. z ) ) +P. ( ( x .P. u ) +P. ( y .P. v ) ) )
53 1 2 3 4 5 6 10 21 32 43 52 ecovdi 
 |-  ( ( A e. R. /\ B e. R. /\ C e. R. ) -> ( A .R ( B +R C ) ) = ( ( A .R B ) +R ( A .R C ) ) )
54 dmaddsr 
 |-  dom +R = ( R. X. R. )
55 0nsr 
 |-  -. (/) e. R.
56 dmmulsr 
 |-  dom .R = ( R. X. R. )
57 54 55 56 ndmovdistr 
 |-  ( -. ( A e. R. /\ B e. R. /\ C e. R. ) -> ( A .R ( B +R C ) ) = ( ( A .R B ) +R ( A .R C ) ) )
58 53 57 pm2.61i 
 |-  ( A .R ( B +R C ) ) = ( ( A .R B ) +R ( A .R C ) )