---

Step * 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) = e ∈ |h|
BY
{ ((RWH (LemmaWithC [`c',f e] `grp_eq_op_l`) 0) THENA 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) * (f e)) = ((f e) * e) ∈ |h|

---

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)  =  e


By

---

Latex:
((RWH  (LemmaWithC  [`c',f  e]  `grp\_eq\_op\_l`)  0)  THENA  Auto)

---

Home Index