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 ⊢ 𝑈 = ( 𝑇 ↾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 𝑇 ) )