---

Step * of Lemma grp_hom_formation

∀[g,h:IGroup]. ∀[f:|g| ⟶ |h|].  IsMonHom{g,h}(f) supposing ∀a,b:|g|.  ((f (a * b)) = ((f a) * (f b)) ∈ |h|)
BY
{ ((AGenRepD ["compound";"basic"]) THEN Auto) }

1
1. g : IGroup
2. h : IGroup
3. f : |g| ⟶ |h|
4. ∀a,b:|g|.  ((f (a * b)) = ((f a) * (f b)) ∈ |h|)
⊢ (f e) = e ∈ |h|

---

Latex:

---

Latex:
\mforall{}[g,h:IGroup].  \mforall{}[f:|g|  {}\mrightarrow{}  |h|].
    IsMonHom\{g,h\}(f)  supposing  \mforall{}a,b:|g|.    ((f  (a  *  b))  =  ((f  a)  *  (f  b)))


By

---

Latex:
((AGenRepD  ["compound";"basic"])  THEN  Auto)

---

Home Index