Metamath Proof Explorer

Theorem ghmmhm

Description: A group homomorphism is a monoid homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015)

Ref Expression
Assertion ghmmhm 
|- ( F e. ( S GrpHom T ) -> F e. ( S MndHom T ) )

Proof

Step Hyp Ref Expression
1 ghmgrp1 
 |-  ( F e. ( S GrpHom T ) -> S e. Grp )
2 grpmnd 
 |-  ( S e. Grp -> S e. Mnd )
3 1 2 syl 
 |-  ( F e. ( S GrpHom T ) -> S e. Mnd )
4 ghmgrp2 
 |-  ( F e. ( S GrpHom T ) -> T e. Grp )
5 grpmnd 
 |-  ( T e. Grp -> T e. Mnd )
6 4 5 syl 
 |-  ( F e. ( S GrpHom T ) -> T e. Mnd )
7 eqid 
 |-  ( Base ` S ) = ( Base ` S )
8 eqid 
 |-  ( Base ` T ) = ( Base ` T )
9 7 8 ghmf 
 |-  ( F e. ( S GrpHom T ) -> F : ( Base ` S ) --> ( Base ` T ) )
10 eqid 
 |-  ( +g ` S ) = ( +g ` S )
11 eqid 
 |-  ( +g ` T ) = ( +g ` T )
12 7 10 11 ghmlin 
 |-  ( ( F e. ( S GrpHom T ) /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
13 12 3expb 
 |-  ( ( F e. ( S GrpHom T ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
14 13 ralrimivva 
 |-  ( F e. ( S GrpHom T ) -> A. x e. ( Base ` S ) A. y e. ( Base ` S ) ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
15 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
16 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
17 15 16 ghmid 
 |-  ( F e. ( S GrpHom T ) -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) )
18 9 14 17 3jca 
 |-  ( F e. ( S GrpHom T ) -> ( F : ( Base ` S ) --> ( Base ` T ) /\ A. x e. ( Base ` S ) A. y e. ( Base ` S ) ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) )
19 7 8 10 11 15 16 ismhm 
 |-  ( F e. ( S MndHom T ) <-> ( ( S e. Mnd /\ T e. Mnd ) /\ ( F : ( Base ` S ) --> ( Base ` T ) /\ A. x e. ( Base ` S ) A. y e. ( Base ` S ) ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) )
20 3 6 18 19 syl21anbrc 
 |-  ( F e. ( S GrpHom T ) -> F e. ( S MndHom T ) )