Metamath Proof Explorer

Theorem ghmgrp1

Description: A group homomorphism is only defined when the domain is a group. (Contributed by Stefan O'Rear, 31-Dec-2014)

Ref Expression
Assertion ghmgrp1 
|- ( F e. ( S GrpHom T ) -> S e. Grp )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` S ) = ( Base ` S )
2 eqid 
 |-  ( Base ` T ) = ( Base ` T )
3 eqid 
 |-  ( +g ` S ) = ( +g ` S )
4 eqid 
 |-  ( +g ` T ) = ( +g ` T )
5 1 2 3 4 isghm 
 |-  ( F e. ( S GrpHom T ) <-> ( ( S e. Grp /\ T e. Grp ) /\ ( F : ( Base ` S ) --> ( Base ` T ) /\ A. y e. ( Base ` S ) A. x e. ( Base ` S ) ( F ` ( y ( +g ` S ) x ) ) = ( ( F ` y ) ( +g ` T ) ( F ` x ) ) ) ) )
6 5 simplbi 
 |-  ( F e. ( S GrpHom T ) -> ( S e. Grp /\ T e. Grp ) )
7 6 simpld 
 |-  ( F e. ( S GrpHom T ) -> S e. Grp )