---

Step * 1 of Lemma bag-summation-minus


1. T : Type
2. r : Rng
3. b : bag(T)
4. f : T ⟶ |r|
⊢ Σ(x∈b). -r f[x] = (-r Σ(x∈b). f[x]) ∈ |r|
BY
{ ((InstLemma `rng_plus_comm` [⌜r⌝]⋅ THEN Auto)
   THEN Fold `comm` (-1)
   THEN (InstLemma `bag-summation-linear1` [⌜T⌝;⌜|r|⌝;⌜+r⌝;⌜*⌝;⌜0⌝;⌜b⌝;⌜f⌝]⋅
         THENA (Auto THEN Try ((With ⌜-r⌝ (D 0)⋅ THEN Auto THEN RepeatFor 2 (DVar `r') THEN Complete (Auto))) THEN Auto)
         )) }

1
1. T : Type
2. r : Rng
3. b : bag(T)
4. f : T ⟶ |r|
5. Comm(|r|;+r)
6. ∀a:|r|. (Σ(x∈b). a * f[x] = (a * Σ(x∈b). f[x]) ∈ |r|)
⊢ Σ(x∈b). -r f[x] = (-r Σ(x∈b). f[x]) ∈ |r|

---

Latex:

---

Latex:

1.  T  :  Type
2.  r  :  Rng
3.  b  :  bag(T)
4.  f  :  T  {}\mrightarrow{}  |r|
\mvdash{}  \mSigma{}(x\mmember{}b).  -r  f[x]  =  (-r  \mSigma{}(x\mmember{}b).  f[x])


By

---

Latex:
((InstLemma  `rng\_plus\_comm`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  Fold  `comm`  (-1)
  THEN  (InstLemma  `bag-summation-linear1`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}|r|\mkleeneclose{};\mkleeneopen{}+r\mkleeneclose{};\mkleeneopen{}*\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}
              THENA  (Auto
                            THEN  Try  ((With  \mkleeneopen{}-r\mkleeneclose{}  (D  0)\mcdot{}
                                                  THEN  Auto
                                                  THEN  RepeatFor  2  (DVar  `r')
                                                  THEN  Complete  (Auto)))
                            THEN  Auto)
              ))

---

Home Index