Metamath Proof Explorer

Theorem ghmmhmb

Description: Group homomorphisms and monoid homomorphisms coincide. (Thus, GrpHom is somewhat redundant, although its stronger reverse closure properties are sometimes useful.) (Contributed by Stefan O'Rear, 7-Mar-2015)

Ref Expression
Assertion ghmmhmb 
|- ( ( S e. Grp /\ T e. Grp ) -> ( S GrpHom T ) = ( S MndHom T ) )

Proof

Step Hyp Ref Expression
1 ghmmhm 
 |-  ( f e. ( S GrpHom T ) -> f e. ( S MndHom T ) )
2 eqid 
 |-  ( Base ` S ) = ( Base ` S )
3 eqid 
 |-  ( Base ` T ) = ( Base ` T )
4 eqid 
 |-  ( +g ` S ) = ( +g ` S )
5 eqid 
 |-  ( +g ` T ) = ( +g ` T )
6 simpll 
 |-  ( ( ( S e. Grp /\ T e. Grp ) /\ f e. ( S MndHom T ) ) -> S e. Grp )
7 simplr 
 |-  ( ( ( S e. Grp /\ T e. Grp ) /\ f e. ( S MndHom T ) ) -> T e. Grp )
8 2 3 mhmf 
 |-  ( f e. ( S MndHom T ) -> f : ( Base ` S ) --> ( Base ` T ) )
9 8 adantl 
 |-  ( ( ( S e. Grp /\ T e. Grp ) /\ f e. ( S MndHom T ) ) -> f : ( Base ` S ) --> ( Base ` T ) )
10 2 4 5 mhmlin 
 |-  ( ( f e. ( S MndHom T ) /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( f ` ( x ( +g ` S ) y ) ) = ( ( f ` x ) ( +g ` T ) ( f ` y ) ) )
11 10 3expb 
 |-  ( ( f e. ( S MndHom T ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( f ` ( x ( +g ` S ) y ) ) = ( ( f ` x ) ( +g ` T ) ( f ` y ) ) )
12 11 adantll 
 |-  ( ( ( ( S e. Grp /\ T e. Grp ) /\ f e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( f ` ( x ( +g ` S ) y ) ) = ( ( f ` x ) ( +g ` T ) ( f ` y ) ) )
13 2 3 4 5 6 7 9 12 isghmd 
 |-  ( ( ( S e. Grp /\ T e. Grp ) /\ f e. ( S MndHom T ) ) -> f e. ( S GrpHom T ) )
14 13 ex 
 |-  ( ( S e. Grp /\ T e. Grp ) -> ( f e. ( S MndHom T ) -> f e. ( S GrpHom T ) ) )
15 1 14 impbid2 
 |-  ( ( S e. Grp /\ T e. Grp ) -> ( f e. ( S GrpHom T ) <-> f e. ( S MndHom T ) ) )
16 15 eqrdv 
 |-  ( ( S e. Grp /\ T e. Grp ) -> ( S GrpHom T ) = ( S MndHom T ) )