---

Step * 2 1 of Lemma bag-summation-linear1


1. T : Type
2. R : Type
3. add : R ⟶ R ⟶ R
4. mul : R ⟶ R ⟶ R
5. zero : R
6. b : bag(T)
7. f : T ⟶ R
8. ∀[g:T ⟶ R]
     ∀a:R. (Σ(x∈b). a mul (f[x] add g[x]) = (a mul (Σ(x∈b). f[x] add Σ(x∈b). g[x])) ∈ R) 
     supposing (∃minus:R ⟶ R. IsGroup(R;add;zero;minus)) ∧ Comm(R;add) ∧ BiLinear(R;add;mul)
9. minus : R ⟶ R
10. IsGroup(R;add;zero;minus)
11. Comm(R;add)
12. BiLinear(R;add;mul)
13. a : R
14. Σ(x∈b). a mul (f[x] add zero) = (a mul (Σ(x∈b). f[x] add Σ(x∈b). zero)) ∈ R
⊢ Σ(x∈b). f[x] = (Σ(x∈b). f[x] add zero) ∈ R
BY
{ (D -5 THEN Symmetry THEN BackThruSomeHyp')⋅ }

---

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.  b  :  bag(T)
7.  f  :  T  {}\mrightarrow{}  R
8.  \mforall{}[g:T  {}\mrightarrow{}  R]
          \mforall{}a:R.  (\mSigma{}(x\mmember{}b).  a  mul  (f[x]  add  g[x])  =  (a  mul  (\mSigma{}(x\mmember{}b).  f[x]  add  \mSigma{}(x\mmember{}b).  g[x]))) 
          supposing  (\mexists{}minus:R  {}\mrightarrow{}  R.  IsGroup(R;add;zero;minus))  \mwedge{}  Comm(R;add)  \mwedge{}  BiLinear(R;add;mul)
9.  minus  :  R  {}\mrightarrow{}  R
10.  IsGroup(R;add;zero;minus)
11.  Comm(R;add)
12.  BiLinear(R;add;mul)
13.  a  :  R
14.  \mSigma{}(x\mmember{}b).  a  mul  (f[x]  add  zero)  =  (a  mul  (\mSigma{}(x\mmember{}b).  f[x]  add  \mSigma{}(x\mmember{}b).  zero))
\mvdash{}  \mSigma{}(x\mmember{}b).  f[x]  =  (\mSigma{}(x\mmember{}b).  f[x]  add  zero)


By

---

Latex:
(D  -5  THEN  Symmetry  THEN  BackThruSomeHyp')\mcdot{}

---

Home Index