---

Step * 1 of Lemma module_hom_is_grp_hom


1. A : Rng@i'
2. m : A-Module@i'
3. n : A-Module@i'
4. f : m.car ⟶ n.car@i
5. module_hom_p(A; m; n; f)@i
⊢ ∀a,b:|(m↓grp)|.  ((f (a * b)) = ((f a) * (f b)) ∈ |(n↓grp)|)
BY
{ ((ARepD ["compound";"basic"] 
THENM Reduce 0 
THENM HypBackchain) THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Rng@i'
2.  m  :  A-Module@i'
3.  n  :  A-Module@i'
4.  f  :  m.car  {}\mrightarrow{}  n.car@i
5.  module\_hom\_p(A;  m;  n;  f)@i
\mvdash{}  \mforall{}a,b:|(m\mdownarrow{}grp)|.    ((f  (a  *  b))  =  ((f  a)  *  (f  b)))


By

---

Latex:
((ARepD  ["compound";"basic"] 
THENM  Reduce  0 
THENM  HypBackchain)  THEN  Auto)

---

Home Index