---

Step * 2 of Lemma bag-summation-hom


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|
BY
{ (D 6 THEN UnfoldTopAb 6 THEN RWO "6" 0 THEN Auto THEN EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  Rng
2.  s  :  Rng
3.  IsMonoid(|s|;+s;0)
4.  IsMonoid(|r|;+r;0)
5.  f  :  |r|  {}\mrightarrow{}  |s|
6.  rng\_hom\_p(r;s;f)
7.  A  :  Type
8.  g  :  A  {}\mrightarrow{}  |r|
9.  u  :  A
10.  v  :  A  List
11.  \mSigma{}(x\mmember{}v).  f[g[x]]  =  f[\mSigma{}(x\mmember{}v).  g[x]]
\mvdash{}  (f[g[u]]  +s  \mSigma{}(x\mmember{}v).  f[g[x]])  =  f[g[u]  +r  \mSigma{}(x\mmember{}v).  g[x]]


By

---

Latex:
(D  6  THEN  UnfoldTopAb  6  THEN  RWO  "6"  0  THEN  Auto  THEN  EqCD  THEN  Auto)

---

Home Index