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

Metamath Proof Explorer

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