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 ↾_{𝑠} ran F$
	Assertion	ghmghmrn	$⊢ F \in (S GrpHom T) \to F \in (S GrpHom U)$

Proof

Step	Hyp	Ref	Expression
1		ghmghmrn.u	$⊢ U = T ↾_{𝑠} ran F$
2		ghmrn	$⊢ F \in (S GrpHom T) \to ran F \in SubGrp (T)$
3		ssid	$⊢ ran F \subseteq ran F$
4	1	resghm2b	$⊢ (ran F \in SubGrp (T) \land ran F \subseteq ran F) \to (F \in (S GrpHom T) \leftrightarrow F \in (S GrpHom U))$
5	3 4	mpan2	$⊢ ran F \in SubGrp (T) \to (F \in (S GrpHom T) \leftrightarrow F \in (S GrpHom U))$
6	5	biimpd	$⊢ ran F \in SubGrp (T) \to (F \in (S GrpHom T) \to F \in (S GrpHom U))$
7	2 6	mpcom	$⊢ F \in (S GrpHom T) \to F \in (S GrpHom U)$