Metamath Proof Explorer

Theorem resghm2b

Description: Restriction of the codomain of a homomorphism. (Contributed by Mario Carneiro, 13-Jan-2015) (Revised by Mario Carneiro, 18-Jun-2015)

Ref Expression
Hypothesis resghm2.u ⊢ 𝑈 = ( 𝑇 ↾s 𝑋 )
Assertion resghm2b ( ( 𝑋 ∈ ( SubGrp ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 resghm2.u ⊢ 𝑈 = ( 𝑇 ↾s 𝑋 )
2 ghmgrp1 ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝑆 ∈ Grp )
3 2 a1i ⊢ ( ( 𝑋 ∈ ( SubGrp ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝑆 ∈ Grp ) )
4 ghmgrp1 ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) → 𝑆 ∈ Grp )
5 4 a1i ⊢ ( ( 𝑋 ∈ ( SubGrp ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) → 𝑆 ∈ Grp ) )
6 subgsubm ⊢ ( 𝑋 ∈ ( SubGrp ‘ 𝑇 ) → 𝑋 ∈ ( SubMnd ‘ 𝑇 ) )
7 1 resmhm2b ⊢ ( ( 𝑋 ∈ ( SubMnd ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ↔ 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) ) )
8 6 7 sylan ⊢ ( ( 𝑋 ∈ ( SubGrp ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ↔ 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) ) )
9 8 adantl ⊢ ( ( 𝑆 ∈ Grp ∧ ( 𝑋 ∈ ( SubGrp ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) ) → ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ↔ 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) ) )
10 subgrcl ⊢ ( 𝑋 ∈ ( SubGrp ‘ 𝑇 ) → 𝑇 ∈ Grp )
11 10 adantr ⊢ ( ( 𝑋 ∈ ( SubGrp ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → 𝑇 ∈ Grp )
12 ghmmhmb ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝑆 GrpHom 𝑇 ) = ( 𝑆 MndHom 𝑇 ) )
13 11 12 sylan2 ⊢ ( ( 𝑆 ∈ Grp ∧ ( 𝑋 ∈ ( SubGrp ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) ) → ( 𝑆 GrpHom 𝑇 ) = ( 𝑆 MndHom 𝑇 ) )
14 13 eleq2d ⊢ ( ( 𝑆 ∈ Grp ∧ ( 𝑋 ∈ ( SubGrp ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ) )
15 1 subggrp ⊢ ( 𝑋 ∈ ( SubGrp ‘ 𝑇 ) → 𝑈 ∈ Grp )
16 15 adantr ⊢ ( ( 𝑋 ∈ ( SubGrp ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → 𝑈 ∈ Grp )
17 ghmmhmb ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑈 ∈ Grp ) → ( 𝑆 GrpHom 𝑈 ) = ( 𝑆 MndHom 𝑈 ) )
18 16 17 sylan2 ⊢ ( ( 𝑆 ∈ Grp ∧ ( 𝑋 ∈ ( SubGrp ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) ) → ( 𝑆 GrpHom 𝑈 ) = ( 𝑆 MndHom 𝑈 ) )
19 18 eleq2d ⊢ ( ( 𝑆 ∈ Grp ∧ ( 𝑋 ∈ ( SubGrp ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) ↔ 𝐹 ∈ ( 𝑆 MndHom 𝑈 ) ) )
20 9 14 19 3bitr4d ⊢ ( ( 𝑆 ∈ Grp ∧ ( 𝑋 ∈ ( SubGrp ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) ) )
21 20 expcom ⊢ ( ( 𝑋 ∈ ( SubGrp ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( 𝑆 ∈ Grp → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) ) ) )
22 3 5 21 pm5.21ndd ⊢ ( ( 𝑋 ∈ ( SubGrp ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) ) )