---

Step * of Lemma module_act_grp_hom_l

∀A:Rng. ∀m:A-Module. ∀u:m.car.  IsMonHom{A↓+gp,m↓grp}(λa:|A|. m.act a u)
BY
{ ((AGenRepD ["compound";"basic"] 
THENM Reduce 0) THENA Auto) }

1
1. A : Rng@i'
2. m : A-Module@i'
3. u : m.car@i
4. a1 : |A↓+gp|
5. a2 : |A↓+gp|
⊢ (m.act (a1 +A a2) u) = ((m.act a1 u) m.plus (m.act a2 u)) ∈ m.car

2
1. A : Rng@i'
2. m : A-Module@i'
3. u : m.car@i
⊢ (m.act 0 u) = m.zero ∈ m.car

---

Latex:

---

Latex:
\mforall{}A:Rng.  \mforall{}m:A-Module.  \mforall{}u:m.car.    IsMonHom\{A\mdownarrow{}+gp,m\mdownarrow{}grp\}(\mlambda{}a:|A|.  m.act  a  u)


By

---

Latex:
((AGenRepD  ["compound";"basic"] 
THENM  Reduce  0)  THENA  Auto)

---

Home Index