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 ) )