---

Step * of Lemma bag-summation-equal2

∀[T:Type]. ∀[r:Rng]. ∀[f,g:T ⟶ |r|]. ∀[b,c:bag(T)].
  Σ(x∈b). f[x] = Σ(x∈c). g[x] ∈ |r| supposing (∀x:T. (x ↓∈ b ⇒ (f[x] = g[x] ∈ |r|))) ∧ (b = c ∈ bag(T))
BY
{ (Auto
   THEN (Assert Assoc(|r|;+r) ∧ Comm(|r|;+r) ∧ IsMonoid(|r|;+r;0) BY
               ((InstLemma `rng_plus_comm` [⌜r⌝]⋅ THENM Fold `comm` (-1))
                THEN Auto
                THEN RepeatFor 2 (DVar `r')
                THEN Auto))
   THEN RevHypSubst' (-2) 0
   THEN Auto
   THEN BLemma `bag-summation-equal`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[r:Rng].  \mforall{}[f,g:T  {}\mrightarrow{}  |r|].  \mforall{}[b,c:bag(T)].
    \mSigma{}(x\mmember{}b).  f[x]  =  \mSigma{}(x\mmember{}c).  g[x]  supposing  (\mforall{}x:T.  (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (f[x]  =  g[x])))  \mwedge{}  (b  =  c)


By

---

Latex:
(Auto
  THEN  (Assert  Assoc(|r|;+r)  \mwedge{}  Comm(|r|;+r)  \mwedge{}  IsMonoid(|r|;+r;0)  BY
                          ((InstLemma  `rng\_plus\_comm`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENM  Fold  `comm`  (-1))
                            THEN  Auto
                            THEN  RepeatFor  2  (DVar  `r')
                            THEN  Auto))
  THEN  RevHypSubst'  (-2)  0
  THEN  Auto
  THEN  BLemma  `bag-summation-equal`
  THEN  Auto)

---

Home Index