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	⊢ 𝑈 = ( 𝑇 ↾s 𝑋 )
Assertion	resghm2	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) ∧ 𝑋 ∈ ( SubGrp ‘ 𝑇 ) ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		resghm2.u	⊢ 𝑈 = ( 𝑇 ↾s 𝑋 )
2		ghmmhm	⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) → 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) )
3		subgsubm	⊢ ( 𝑋 ∈ ( SubGrp ‘ 𝑇 ) → 𝑋 ∈ ( SubMnd ‘ 𝑇 ) )
4	1	resmhm2	⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ) → 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) )
5	2 3 4	syl2an	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) ∧ 𝑋 ∈ ( SubGrp ‘ 𝑇 ) ) → 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) )
6		ghmgrp1	⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) → 𝑆 ∈ Grp )
7		subgrcl	⊢ ( 𝑋 ∈ ( SubGrp ‘ 𝑇 ) → 𝑇 ∈ Grp )
8		ghmmhmb	⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝑆 GrpHom 𝑇 ) = ( 𝑆 MndHom 𝑇 ) )
9	6 7 8	syl2an	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) ∧ 𝑋 ∈ ( SubGrp ‘ 𝑇 ) ) → ( 𝑆 GrpHom 𝑇 ) = ( 𝑆 MndHom 𝑇 ) )
10	5 9	eleqtrrd	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) ∧ 𝑋 ∈ ( SubGrp ‘ 𝑇 ) ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )