---

Step * of Lemma bag-summation-ring-linear1

∀[T:Type]. ∀[r:Rng]. ∀[b:bag(T)]. ∀[f:T ⟶ |r|].
  ∀a:|r|. ((Σ(x∈b). f[x] * a = (Σ(x∈b). f[x] * a) ∈ |r|) ∧ (Σ(x∈b). a * f[x] = (a * Σ(x∈b). f[x]) ∈ |r|))
BY
{ (Auto
   THEN ((InstLemma `rng_plus_comm` [⌜r⌝]⋅ THENA Auto) THEN Fold `comm` (-1))
   THEN (Assert BiLinear(|r|;+r;*) ∧ (∃minus:|r| ⟶ |r|. IsGroup(|r|;+r;0;minus)) BY
               (Auto THEN Try ((With ⌜-r⌝ (D 0)⋅ THEN Auto THEN RepeatFor 2 (DVar `r') THEN Complete (Auto)))))
   THEN Try ((BLemma `bag-summation-linear1` THEN Auto))
   THEN Try ((BLemma `bag-summation-linear1-right` THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[r:Rng].  \mforall{}[b:bag(T)].  \mforall{}[f:T  {}\mrightarrow{}  |r|].
    \mforall{}a:|r|.  ((\mSigma{}(x\mmember{}b).  f[x]  *  a  =  (\mSigma{}(x\mmember{}b).  f[x]  *  a))  \mwedge{}  (\mSigma{}(x\mmember{}b).  a  *  f[x]  =  (a  *  \mSigma{}(x\mmember{}b).  f[x])))


By

---

Latex:
(Auto
  THEN  ((InstLemma  `rng\_plus\_comm`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  Fold  `comm`  (-1))
  THEN  (Assert  BiLinear(|r|;+r;*)  \mwedge{}  (\mexists{}minus:|r|  {}\mrightarrow{}  |r|.  IsGroup(|r|;+r;0;minus))  BY
                          (Auto
                            THEN  Try  ((With  \mkleeneopen{}-r\mkleeneclose{}  (D  0)\mcdot{}
                                                  THEN  Auto
                                                  THEN  RepeatFor  2  (DVar  `r')
                                                  THEN  Complete  (Auto)))
                            ))
  THEN  Try  ((BLemma  `bag-summation-linear1`  THEN  Auto))
  THEN  Try  ((BLemma  `bag-summation-linear1-right`  THEN  Auto)))

---

Home Index