---

Step * of Lemma bag-summation-is-zero

∀[T,R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[f:T ⟶ R].
  Σ(x∈b). f[x] = zero ∈ R supposing (∀x:T. (x ↓∈ b ⇒ (f[x] = zero ∈ R))) ∧ IsMonoid(R;add;zero) ∧ Comm(R;add)
BY
{ (Auto
   THEN ((Assert Σ(x∈b). f[x] = Σ(x∈b). zero ∈ R BY
                ((InstLemma `bag-summation-equal` [⌜T⌝;⌜R⌝;⌜add⌝;⌜zero⌝]⋅ THENA Auto) THEN BHyp -1  THEN Auto))
         THEN RWO "bag-summation-zero" (-1)
         THEN Auto)⋅
   ) }

---

Latex:

---

Latex:
\mforall{}[T,R:Type].  \mforall{}[add:R  {}\mrightarrow{}  R  {}\mrightarrow{}  R].  \mforall{}[zero:R].  \mforall{}[b:bag(T)].  \mforall{}[f:T  {}\mrightarrow{}  R].
    \mSigma{}(x\mmember{}b).  f[x]  =  zero 
    supposing  (\mforall{}x:T.  (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (f[x]  =  zero)))  \mwedge{}  IsMonoid(R;add;zero)  \mwedge{}  Comm(R;add)


By

---

Latex:
(Auto
  THEN  ((Assert  \mSigma{}(x\mmember{}b).  f[x]  =  \mSigma{}(x\mmember{}b).  zero  BY
                            ((InstLemma  `bag-summation-equal`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{};\mkleeneopen{}add\mkleeneclose{};\mkleeneopen{}zero\mkleeneclose{}]\mcdot{}  THENA  Auto)
                              THEN  BHyp  -1 
                              THEN  Auto))
              THEN  RWO  "bag-summation-zero"  (-1)
              THEN  Auto)\mcdot{}
  )

---

Home Index