Step |
Hyp |
Ref |
Expression |
1 |
|
zrrhm.b |
|- B = ( Base ` T ) |
2 |
|
zrrhm.0 |
|- .0. = ( 0g ` S ) |
3 |
|
zrrhm.h |
|- H = ( x e. B |-> .0. ) |
4 |
|
c0snmhm.z |
|- Z = ( 0g ` T ) |
5 |
|
grpmnd |
|- ( S e. Grp -> S e. Mnd ) |
6 |
|
grpmnd |
|- ( T e. Grp -> T e. Mnd ) |
7 |
|
id |
|- ( B = { Z } -> B = { Z } ) |
8 |
1 2 3 4
|
c0snmhm |
|- ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> H e. ( T MndHom S ) ) |
9 |
5 6 7 8
|
syl3an |
|- ( ( S e. Grp /\ T e. Grp /\ B = { Z } ) -> H e. ( T MndHom S ) ) |
10 |
|
ghmmhmb |
|- ( ( T e. Grp /\ S e. Grp ) -> ( T GrpHom S ) = ( T MndHom S ) ) |
11 |
10
|
eleq2d |
|- ( ( T e. Grp /\ S e. Grp ) -> ( H e. ( T GrpHom S ) <-> H e. ( T MndHom S ) ) ) |
12 |
11
|
ancoms |
|- ( ( S e. Grp /\ T e. Grp ) -> ( H e. ( T GrpHom S ) <-> H e. ( T MndHom S ) ) ) |
13 |
12
|
3adant3 |
|- ( ( S e. Grp /\ T e. Grp /\ B = { Z } ) -> ( H e. ( T GrpHom S ) <-> H e. ( T MndHom S ) ) ) |
14 |
9 13
|
mpbird |
|- ( ( S e. Grp /\ T e. Grp /\ B = { Z } ) -> H e. ( T GrpHom S ) ) |