---

Step * of Lemma bag-summation-hom

∀[r,s:Rng]. ∀[f:|r| ⟶ |s|].
  ∀[A:Type]. ∀[g:A ⟶ |r|]. ∀[b:bag(A)].  (Σ(x∈b). f[g[x]] = f[Σ(x∈b). g[x]] ∈ |s|) supposing rng_hom_p(r;s;f)
BY
{ (Auto
   THEN (Assert IsMonoid(|s|;+s;0) ∧ IsMonoid(|r|;+r;0) BY
               (RepeatFor 2 (D 0) THEN Auto))
   THEN PromoteHyp (-1) 3
   THEN BagToList (-1)
   THEN Auto
   THEN ListInd (-1)
   THEN Folds ``cons-bag empty-bag`` 0
   THEN RWO "bag-summation-empty bag-summation-cons" 0
   THEN Auto) }

1
1. r : Rng
2. s : Rng
3. IsMonoid(|s|;+s;0)
4. IsMonoid(|r|;+r;0)
5. f : |r| ⟶ |s|
6. rng_hom_p(r;s;f)
7. A : Type
8. g : A ⟶ |r|
⊢ 0 = f[0] ∈ |s|

2
1. r : Rng
2. s : Rng
3. IsMonoid(|s|;+s;0)
4. IsMonoid(|r|;+r;0)
5. f : |r| ⟶ |s|
6. rng_hom_p(r;s;f)
7. A : Type
8. g : A ⟶ |r|
9. u : A
10. v : A List
11. Σ(x∈v). f[g[x]] = f[Σ(x∈v). g[x]] ∈ |s|
⊢ (f[g[u]] +s Σ(x∈v). f[g[x]]) = f[g[u] +r Σ(x∈v). g[x]] ∈ |s|

---

Latex:

---

Latex:
\mforall{}[r,s:Rng].  \mforall{}[f:|r|  {}\mrightarrow{}  |s|].
    \mforall{}[A:Type].  \mforall{}[g:A  {}\mrightarrow{}  |r|].  \mforall{}[b:bag(A)].    (\mSigma{}(x\mmember{}b).  f[g[x]]  =  f[\mSigma{}(x\mmember{}b).  g[x]]) 
    supposing  rng\_hom\_p(r;s;f)


By

---

Latex:
(Auto
  THEN  (Assert  IsMonoid(|s|;+s;0)  \mwedge{}  IsMonoid(|r|;+r;0)  BY
                          (RepeatFor  2  (D  0)  THEN  Auto))
  THEN  PromoteHyp  (-1)  3
  THEN  BagToList  (-1)
  THEN  Auto
  THEN  ListInd  (-1)
  THEN  Folds  ``cons-bag  empty-bag``  0
  THEN  RWO  "bag-summation-empty  bag-summation-cons"  0
  THEN  Auto)

---

Home Index