---

Step * of Lemma bag-summation-product

∀[r:Rng]. ∀[A,B:Type]. ∀[f:A ⟶ |r|]. ∀[c:bag(B)]. ∀[g:B ⟶ |r|]. ∀[b:bag(A)].
  ((Σ(x∈b). f[x] * Σ(y∈c). g[y]) = Σ(p∈b × c). f[fst(p)] * g[snd(p)] ∈ |r|)
BY
{ (Auto
   THEN (InstLemma `rng_plus_comm` [⌜r⌝]⋅ THENA Auto)
   THEN Fold `comm` (-1)
   THEN (Assert Assoc(|r|;+r) BY
               (RepeatFor 2 (DVar `r') THEN Auto))
   THEN PromoteHyp (-2) 2
   THEN PromoteHyp (-1) 2
   THEN (BagInd (-1) THENA Auto)⋅) }

1
1. r : Rng
2. Assoc(|r|;+r)
3. Comm(|r|;+r)
4. A : Type
5. B : Type
6. f : A ⟶ |r|
7. c : bag(B)
8. g : B ⟶ |r|
⊢ (Σ(x∈[]). f[x] * Σ(y∈c). g[y]) = Σ(p∈[] × c). f[fst(p)] * g[snd(p)] ∈ |r|

2
1. r : Rng
2. Assoc(|r|;+r)
3. Comm(|r|;+r)
4. A : Type
5. B : Type
6. f : A ⟶ |r|
7. c : bag(B)
8. g : B ⟶ |r|
9. u : A
10. v : A List
11. (Σ(x∈v). f[x] * Σ(y∈c). g[y]) = Σ(p∈v × c). f[fst(p)] * g[snd(p)] ∈ |r|
⊢ (Σ(x∈[u / v]). f[x] * Σ(y∈c). g[y]) = Σ(p∈[u / v] × c). f[fst(p)] * g[snd(p)] ∈ |r|

---

Latex:

---

Latex:
\mforall{}[r:Rng].  \mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  |r|].  \mforall{}[c:bag(B)].  \mforall{}[g:B  {}\mrightarrow{}  |r|].  \mforall{}[b:bag(A)].
    ((\mSigma{}(x\mmember{}b).  f[x]  *  \mSigma{}(y\mmember{}c).  g[y])  =  \mSigma{}(p\mmember{}b  \mtimes{}  c).  f[fst(p)]  *  g[snd(p)])


By

---

Latex:
(Auto
  THEN  (InstLemma  `rng\_plus\_comm`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Fold  `comm`  (-1)
  THEN  (Assert  Assoc(|r|;+r)  BY
                          (RepeatFor  2  (DVar  `r')  THEN  Auto))
  THEN  PromoteHyp  (-2)  2
  THEN  PromoteHyp  (-1)  2
  THEN  (BagInd  (-1)  THENA  Auto)\mcdot{})

---

Home Index