---

Step * 1 1 of Lemma grp_hom_formation


1. g : IGroup
2. h : IGroup
3. f : |g| ⟶ |h|
4. ∀a,b:|g|.  ((f (a * b)) = ((f a) * (f b)) ∈ |h|)
⊢ ((f e) * (f e)) = ((f e) * e) ∈ |h|
BY
{ ((RWO "4<" 0 THENM RW GrpNormC 0) THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  IGroup
2.  h  :  IGroup
3.  f  :  |g|  {}\mrightarrow{}  |h|
4.  \mforall{}a,b:|g|.    ((f  (a  *  b))  =  ((f  a)  *  (f  b)))
\mvdash{}  ((f  e)  *  (f  e))  =  ((f  e)  *  e)


By

---

Latex:
((RWO  "4<"  0  THENM  RW  GrpNormC  0)  THEN  Auto)

---

Home Index