---

Step * of Lemma mod_mssum_swap

∀r:Rng. ∀m:r-Module. ∀s,s':DSet. ∀f:|s| ⟶ |s'| ⟶ m.car. ∀a:MSet{s}. ∀b:MSet{s'}.
  ((Σm x ∈ a. Σm y ∈ b. f[x;y]) = (Σm y ∈ b. Σm x ∈ a. f[x;y]) ∈ m.car)
BY
{ ProveSpecializedLemma `mset_for_swap` 2 [parm{i};m↓grp] ((TryC (FoldsC ``mod_mssum``) ANDTHENC AbReduceC)) }

---

Latex:

---

Latex:
\mforall{}r:Rng.  \mforall{}m:r-Module.  \mforall{}s,s':DSet.  \mforall{}f:|s|  {}\mrightarrow{}  |s'|  {}\mrightarrow{}  m.car.  \mforall{}a:MSet\{s\}.  \mforall{}b:MSet\{s'\}.
    ((\mSigma{}m  x  \mmember{}  a.  \mSigma{}m  y  \mmember{}  b.  f[x;y])  =  (\mSigma{}m  y  \mmember{}  b.  \mSigma{}m  x  \mmember{}  a.  f[x;y]))


By

---

Latex:
ProveSpecializedLemma  `mset\_for\_swap`  2  [parm\{i\};m\mdownarrow{}grp
]  ((TryC  (FoldsC  ``mod\_mssum``)  ANDTHENC  AbReduceC))

---

Home Index