---

Step * 1 1 2 1 1 1 1 of Lemma bag-summation-linear-right


1. T : Type
2. R : Type
3. add : R ⟶ R ⟶ R
4. mul : R ⟶ R ⟶ R
5. zero : R
6. f : T ⟶ R
7. g : T ⟶ R
8. minus : R ⟶ R
9. IsGroup(R;add;zero;minus)
10. Comm(R;add)
11. ∀[a,x,y:R].
      (((a mul (x add y)) = ((a mul x) add (a mul y)) ∈ R) ∧ (((x add y) mul a) = ((x mul a) add (y mul a)) ∈ R))
12. a : R
13. u : T
14. v : T List
15. ∀x,y,z:R.
      ((z = mul[add[x;y];a] ∈ R)
      ⇒ (accumulate (with value c and list item x):
           add mul[add[f[x];g[x]];a] c
          over list:
            v
          with starting value:
           z)
         = mul[add[accumulate (with value c and list item x):
                    add f[x] c
                   over list:
                     v
                   with starting value:
                    x);accumulate (with value c and list item x):
                        add g[x] c
                       over list:
                         v
                       with starting value:
                        y)];a]
         ∈ R))
16. x : R
17. y : R
18. z : R
19. z = mul[add[x;y];a] ∈ R
⊢ ((((f u) mul a) add ((g u) mul a)) add ((x mul a) add (y mul a)))
= ((((f u) mul a) add (x mul a)) add (((g u) mul a) add (y mul a)))
∈ R
BY
{ (RepUR ``group_p monoid_p assoc`` 9
   THEN Auto
   THEN RWW "9" 0
   THEN Auto
   THEN EqCD
   THEN Auto
   THEN RWW "9<" 0
   THEN Auto
   THEN EqCD
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  Type
3.  add  :  R  {}\mrightarrow{}  R  {}\mrightarrow{}  R
4.  mul  :  R  {}\mrightarrow{}  R  {}\mrightarrow{}  R
5.  zero  :  R
6.  f  :  T  {}\mrightarrow{}  R
7.  g  :  T  {}\mrightarrow{}  R
8.  minus  :  R  {}\mrightarrow{}  R
9.  IsGroup(R;add;zero;minus)
10.  Comm(R;add)
11.  \mforall{}[a,x,y:R].
            (((a  mul  (x  add  y))  =  ((a  mul  x)  add  (a  mul  y)))
            \mwedge{}  (((x  add  y)  mul  a)  =  ((x  mul  a)  add  (y  mul  a))))
12.  a  :  R
13.  u  :  T
14.  v  :  T  List
15.  \mforall{}x,y,z:R.
            ((z  =  mul[add[x;y];a])
            {}\mRightarrow{}  (accumulate  (with  value  c  and  list  item  x):
                      add  mul[add[f[x];g[x]];a]  c
                    over  list:
                        v
                    with  starting  value:
                      z)
                  =  mul[add[accumulate  (with  value  c  and  list  item  x):
                                        add  f[x]  c
                                      over  list:
                                          v
                                      with  starting  value:
                                        x);accumulate  (with  value  c  and  list  item  x):
                                                add  g[x]  c
                                              over  list:
                                                  v
                                              with  starting  value:
                                                y)];a]))
16.  x  :  R
17.  y  :  R
18.  z  :  R
19.  z  =  mul[add[x;y];a]
\mvdash{}  ((((f  u)  mul  a)  add  ((g  u)  mul  a))  add  ((x  mul  a)  add  (y  mul  a)))
=  ((((f  u)  mul  a)  add  (x  mul  a))  add  (((g  u)  mul  a)  add  (y  mul  a)))


By

---

Latex:
(RepUR  ``group\_p  monoid\_p  assoc``  9
  THEN  Auto
  THEN  RWW  "9"  0
  THEN  Auto
  THEN  EqCD
  THEN  Auto
  THEN  RWW  "9<"  0
  THEN  Auto
  THEN  EqCD
  THEN  Auto)

---

Home Index