Step * 1 of Lemma grp_hom_formation


1. IGroup
2. IGroup
3. |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. IGroup
2. IGroup
3. |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