---

Step * of Lemma fabmon_of_nat_mcp_wf

∀s:DSet. ∀m:MCopower(s;<ℤ+>↓hgrp).  (fabmon_of_nat_mcp(m) ∈ FAbMon(s))
BY
{ ((Unfold `fabmon_of_nat_mcp` 0  
THEN RepD  
THENM BLemma `mk_fabmon`  
THENM GenRepD) THENA Auto) }

1
1. s : DSet
2. m : MCopower(s;<ℤ+>↓hgrp)
3. g' : AbMon
4. f : |s| ⟶ |g'|
⊢ IsMonHom{m.mon,g'}((λm',f. (m.umap m' (λz,n. (nat(n) ⋅ (f z))))) g' f)

2
1. s : DSet
2. m : MCopower(s;<ℤ+>↓hgrp)
3. g' : AbMon
4. f : |s| ⟶ |g'|
⊢ (((λm',f. (m.umap m' (λz,n. (nat(n) ⋅ (f z))))) g' f) o (λu.(m.inj u zhgrp(1)))) = f ∈ (|s| ⟶ |g'|)

3
1. s : DSet
2. m : MCopower(s;<ℤ+>↓hgrp)
3. g' : AbMon
4. f : |s| ⟶ |g'|
5. u : |m.mon| ⟶ |g'|
6. IsMonHom{m.mon,g'}(u)
7. (u o (λu.(m.inj u zhgrp(1)))) = f ∈ (|s| ⟶ |g'|)
⊢ u = ((λm',f. (m.umap m' (λz,n. (nat(n) ⋅ (f z))))) g' f) ∈ (|m.mon| ⟶ |g'|)

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}m:MCopower(s;<\mBbbZ{}+>\mdownarrow{}hgrp).    (fabmon\_of\_nat\_mcp(m)  \mmember{}  FAbMon(s))


By

---

Latex:
((Unfold  `fabmon\_of\_nat\_mcp`  0   
THEN  RepD   
THENM  BLemma  `mk\_fabmon`   
THENM  GenRepD)  THENA  Auto)

---

Home Index