Theorem resghm2

Description: One direction of resghm2b . (Contributed by Mario Carneiro, 13-Jan-2015) (Revised by Mario Carneiro, 18-Jun-2015)

	Ref	Expression
Hypothesis	resghm2.u	|- U = ( T |`s X )
Assertion	resghm2	|- ( ( F e. ( S GrpHom U ) /\ X e. ( SubGrp ` T ) ) -> F e. ( S GrpHom T ) )

Proof

Step	Hyp	Ref	Expression
1		resghm2.u	|- U = ( T |`s X )
2		ghmmhm	|- ( F e. ( S GrpHom U ) -> F e. ( S MndHom U ) )
3		subgsubm	|- ( X e. ( SubGrp ` T ) -> X e. ( SubMnd ` T ) )
4	1	resmhm2	|- ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) -> F e. ( S MndHom T ) )
5	2 3 4	syl2an	|- ( ( F e. ( S GrpHom U ) /\ X e. ( SubGrp ` T ) ) -> F e. ( S MndHom T ) )
6		ghmgrp1	|- ( F e. ( S GrpHom U ) -> S e. Grp )
7		subgrcl	|- ( X e. ( SubGrp ` T ) -> T e. Grp )
8		ghmmhmb	|- ( ( S e. Grp /\ T e. Grp ) -> ( S GrpHom T ) = ( S MndHom T ) )
9	6 7 8	syl2an	|- ( ( F e. ( S GrpHom U ) /\ X e. ( SubGrp ` T ) ) -> ( S GrpHom T ) = ( S MndHom T ) )
10	5 9	eleqtrrd	|- ( ( F e. ( S GrpHom U ) /\ X e. ( SubGrp ` T ) ) -> F e. ( S GrpHom T ) )