---

Step * 1 of Lemma module_act_is_grp_hom


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
BY
{ ((BLemma `module_act_plus`) THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Rng@i'
2.  m  :  A-Module@i'
3.  a  :  |A|@i
4.  a1  :  |(m\mdownarrow{}grp)|
5.  a2  :  |(m\mdownarrow{}grp)|
\mvdash{}  (m.act  a  (a1  m.plus  a2))  =  ((m.act  a  a1)  m.plus  (m.act  a  a2))


By

---

Latex:
((BLemma  `module\_act\_plus`)  THEN  Auto)

---

Home Index