---

Step * 1 2 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)
6. u : |a|
7. a@0 : omral_alg(g;a).car
⊢ (alg_umap(n,f) (omral_alg(g;a).act u a@0)) = (n.act u (alg_umap(n,f) a@0)) ∈ n.car
BY
{ RenameVar `a1' (-1) 
THENM 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)
6. u : |a|
7. a1 : |omral(g;a)|
⊢ (Σk ∈ dom(u ⋅⋅ a1). (((u ⋅⋅ a1)[k]) n.act (f k))) = (n.act u (Σk ∈ dom(a1). ((a1[k]) n.act (f k)))) ∈ 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)
6.  u  :  |a|
7.  a@0  :  omral\_alg(g;a).car
\mvdash{}  (alg\_umap(n,f)  (omral\_alg(g;a).act  u  a@0))  =  (n.act  u  (alg\_umap(n,f)  a@0))


By

---

Latex:
RenameVar  `a1'  (-1) 
THENM  All  (RW  (HigherC  AbRedexC)) 
THENM  Force  `5`  (Eval  ``omral\_alg\_umap``  0)

---

Home Index