---

Step * 1 4 of Lemma omral_alg_umap_is_hom


1. g : OCMon
2. g ∈ DMon
3. a : CDRng
4. n : algebra{i:l}(a)
5. f : MonHom(g,n↓rg↓xmn)
⊢ (alg_umap(n,f) omral_alg(g;a).one) = n.one ∈ n.car
BY
{ All (RW (HigherC AbRedexC)) 
THENM Force `5` (Eval ``omral_alg_umap`` 0) }

1
1. g : OCMon
2. g ∈ DMon
3. a : CDRng
4. n : algebra{i:l}(a)
5. f : MonHom(g,n↓rg↓xmn)
⊢ (Σk ∈ dom(11). ((11[k]) n.act (f k))) = n.one ∈ n.car

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  g  \mmember{}  DMon
3.  a  :  CDRng
4.  n  :  algebra\{i:l\}(a)
5.  f  :  MonHom(g,n\mdownarrow{}rg\mdownarrow{}xmn)
\mvdash{}  (alg\_umap(n,f)  omral\_alg(g;a).one)  =  n.one


By

---

Latex:
All  (RW  (HigherC  AbRedexC)) 
THENM  Force  `5`  (Eval  ``omral\_alg\_umap``  0)

---

Home Index