---

Step * of Lemma module_act_is_grp_hom

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

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

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

---

Latex:

---

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


By

---

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

---

Home Index