resghm2

		Ref	Expression
	Hypothesis	resghm2.u	$⊢ U = T ↾_{𝑠} X$
	Assertion	resghm2	$⊢ (F \in (S GrpHom U) \land X \in SubGrp (T)) \to F \in (S GrpHom T)$

Step	Hyp	Ref	Expression
1		resghm2.u	$⊢ U = T ↾_{𝑠} X$
2		ghmmhm	$⊢ F \in (S GrpHom U) \to F \in (S MndHom U)$
3		subgsubm	$⊢ X \in SubGrp (T) \to X \in SubMnd (T)$
4	1	resmhm2	$⊢ (F \in (S MndHom U) \land X \in SubMnd (T)) \to F \in (S MndHom T)$
5	2 3 4	syl2an	$⊢ (F \in (S GrpHom U) \land X \in SubGrp (T)) \to F \in (S MndHom T)$
6		ghmgrp1	$⊢ F \in (S GrpHom U) \to S \in Grp$
7		subgrcl	$⊢ X \in SubGrp (T) \to T \in Grp$
8		ghmmhmb	$⊢ (S \in Grp \land T \in Grp) \to S GrpHom T = S MndHom T$
9	6 7 8	syl2an	$⊢ (F \in (S GrpHom U) \land X \in SubGrp (T)) \to S GrpHom T = S MndHom T$
10	5 9	eleqtrrd	$⊢ (F \in (S GrpHom U) \land X \in SubGrp (T)) \to F \in (S GrpHom T)$

Metamath Proof Explorer