This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ghmghmrn

Description: A group homomorphism from G to H is also a group homomorphism from G to its image in H . (Contributed by Paul Chapman, 3-Mar-2008) (Revised by AV, 26-Aug-2021)

Ref Expression
Hypothesis ghmghmrn.u 
|- U = ( T |`s ran F )
Assertion ghmghmrn 
|- ( F e. ( S GrpHom T ) -> F e. ( S GrpHom U ) )

Proof

Step Hyp Ref Expression
1 ghmghmrn.u 
 |-  U = ( T |`s ran F )
2 ghmrn 
 |-  ( F e. ( S GrpHom T ) -> ran F e. ( SubGrp ` T ) )
3 ssid 
 |-  ran F C_ ran F
4 1 resghm2b 
 |-  ( ( ran F e. ( SubGrp ` T ) /\ ran F C_ ran F ) -> ( F e. ( S GrpHom T ) <-> F e. ( S GrpHom U ) ) )
5 3 4 mpan2 
 |-  ( ran F e. ( SubGrp ` T ) -> ( F e. ( S GrpHom T ) <-> F e. ( S GrpHom U ) ) )
6 5 biimpd 
 |-  ( ran F e. ( SubGrp ` T ) -> ( F e. ( S GrpHom T ) -> F e. ( S GrpHom U ) ) )
7 2 6 mpcom 
 |-  ( F e. ( S GrpHom T ) -> F e. ( S GrpHom U ) )