---

Step * 1 1 of Lemma bag-summation-linear1-right

.....subterm..... T:t
2:n
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). (f[x] add g[x]) mul a = ((Σ(x∈b). f[x] add Σ(x∈b). g[x]) mul a) ∈ 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). (f[x] add zero) mul a = ((Σ(x∈b). f[x] add Σ(x∈b). zero) mul a) ∈ R
15. x : T
⊢ f[x] = (f[x] add zero) ∈ R
BY
{ (D -6 THEN Symmetry THEN Auto') }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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).  (f[x]  add  g[x])  mul  a  =  ((\mSigma{}(x\mmember{}b).  f[x]  add  \mSigma{}(x\mmember{}b).  g[x])  mul  a)) 
          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).  (f[x]  add  zero)  mul  a  =  ((\mSigma{}(x\mmember{}b).  f[x]  add  \mSigma{}(x\mmember{}b).  zero)  mul  a)
15.  x  :  T
\mvdash{}  f[x]  =  (f[x]  add  zero)


By

---

Latex:
(D  -6  THEN  Symmetry  THEN  Auto')

---

Home Index