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 1 grpmndd 
 |-  ( F e. ( S GrpHom T ) -> S e. Mnd )
3 ghmgrp2 
 |-  ( F e. ( S GrpHom T ) -> T e. Grp )
4 3 grpmndd 
 |-  ( F e. ( S GrpHom T ) -> T e. Mnd )
5 eqid 
 |-  ( Base ` S ) = ( Base ` S )
6 eqid 
 |-  ( Base ` T ) = ( Base ` T )
7 5 6 ghmf 
 |-  ( F e. ( S GrpHom T ) -> F : ( Base ` S ) --> ( Base ` T ) )
8 eqid 
 |-  ( +g ` S ) = ( +g ` S )
9 eqid 
 |-  ( +g ` T ) = ( +g ` T )
10 5 8 9 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 ) ) )
11 10 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 ) ) )
12 11 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 ) ) )
13 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
14 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
15 13 14 ghmid 
 |-  ( F e. ( S GrpHom T ) -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) )
16 7 12 15 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 ) ) )
17 5 6 8 9 13 14 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 ) ) ) )
18 2 4 16 17 syl21anbrc 
 |-  ( F e. ( S GrpHom T ) -> F e. ( S MndHom T ) )