---

Step * 1 of Lemma module_act_grp_hom_l


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index