Metamath Proof Explorer

Theorem ghomf

Description: Mapping property of a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009)

Ref Expression
Hypotheses ghomf.1 
|- X = ran G
ghomf.2 
|- W = ran H
Assertion ghomf 
|- ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> F : X --> W )

Proof

Step Hyp Ref Expression
1 ghomf.1 
 |-  X = ran G
2 ghomf.2 
 |-  W = ran H
3 1 2 elghomOLD 
 |-  ( ( G e. GrpOp /\ H e. GrpOp ) -> ( F e. ( G GrpOpHom H ) <-> ( F : X --> W /\ A. x e. X A. y e. X ( ( F ` x ) H ( F ` y ) ) = ( F ` ( x G y ) ) ) ) )
4 3 simprbda 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp ) /\ F e. ( G GrpOpHom H ) ) -> F : X --> W )
5 4 3impa 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> F : X --> W )