---

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


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. BiLinear(R;add;mul)
12. a : R
13. u : T
14. v : T List
15. ∀x,y,z:R.
      ((z = mul[a;add[x;y]] ∈ R)
      ⇒ (accumulate (with value c and list item x):
           add mul[a;add[f[x];g[x]]] c
          over list:
            v
          with starting value:
           z)
         = mul[a;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)]]
         ∈ R))
16. x : R
17. y : R
18. z : R
19. z = mul[a;add[x;y]] ∈ R
⊢ (add mul[a;add[f[u];g[u]]] z) = mul[a;add[add f[u] x;add g[u] y]] ∈ R
BY
{ (HypSubst (-1) 0 THEN Auto) }

1
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. BiLinear(R;add;mul)
12. a : R
13. u : T
14. v : T List
15. ∀x,y,z:R.
      ((z = mul[a;add[x;y]] ∈ R)
      ⇒ (accumulate (with value c and list item x):
           add mul[a;add[f[x];g[x]]] c
          over list:
            v
          with starting value:
           z)
         = mul[a;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)]]
         ∈ R))
16. x : R
17. y : R
18. z : R
19. z = mul[a;add[x;y]] ∈ R
⊢ (add mul[a;add[f[u];g[u]]] mul[a;add[x;y]]) = mul[a;add[add f[u] x;add g[u] y]] ∈ R

---

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.  BiLinear(R;add;mul)
12.  a  :  R
13.  u  :  T
14.  v  :  T  List
15.  \mforall{}x,y,z:R.
            ((z  =  mul[a;add[x;y]])
            {}\mRightarrow{}  (accumulate  (with  value  c  and  list  item  x):
                      add  mul[a;add[f[x];g[x]]]  c
                    over  list:
                        v
                    with  starting  value:
                      z)
                  =  mul[a;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)]]))
16.  x  :  R
17.  y  :  R
18.  z  :  R
19.  z  =  mul[a;add[x;y]]
\mvdash{}  (add  mul[a;add[f[u];g[u]]]  z)  =  mul[a;add[add  f[u]  x;add  g[u]  y]]


By

---

Latex:
(HypSubst  (-1)  0  THEN  Auto)

---

Home Index