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 ⊢ U = T ↾ 𝑠 X
Assertion resghm2b ⊢ X ∈ SubGrp ⁡ T ∧ ran ⁡ F ⊆ X → F ∈ S GrpHom T ↔ F ∈ S GrpHom U

Proof

Step Hyp Ref Expression
1 resghm2.u ⊢ U = T ↾ 𝑠 X
2 ghmgrp1 ⊢ F ∈ S GrpHom T → S ∈ Grp
3 2 a1i ⊢ X ∈ SubGrp ⁡ T ∧ ran ⁡ F ⊆ X → F ∈ S GrpHom T → S ∈ Grp
4 ghmgrp1 ⊢ F ∈ S GrpHom U → S ∈ Grp
5 4 a1i ⊢ X ∈ SubGrp ⁡ T ∧ ran ⁡ F ⊆ X → F ∈ S GrpHom U → S ∈ Grp
6 subgsubm ⊢ X ∈ SubGrp ⁡ T → X ∈ SubMnd ⁡ T
7 1 resmhm2b ⊢ X ∈ SubMnd ⁡ T ∧ ran ⁡ F ⊆ X → F ∈ S MndHom T ↔ F ∈ S MndHom U
8 6 7 sylan ⊢ X ∈ SubGrp ⁡ T ∧ ran ⁡ F ⊆ X → F ∈ S MndHom T ↔ F ∈ S MndHom U
9 8 adantl ⊢ S ∈ Grp ∧ X ∈ SubGrp ⁡ T ∧ ran ⁡ F ⊆ X → F ∈ S MndHom T ↔ F ∈ S MndHom U
10 subgrcl ⊢ X ∈ SubGrp ⁡ T → T ∈ Grp
11 10 adantr ⊢ X ∈ SubGrp ⁡ T ∧ ran ⁡ F ⊆ X → T ∈ Grp
12 ghmmhmb ⊢ S ∈ Grp ∧ T ∈ Grp → S GrpHom T = S MndHom T
13 11 12 sylan2 ⊢ S ∈ Grp ∧ X ∈ SubGrp ⁡ T ∧ ran ⁡ F ⊆ X → S GrpHom T = S MndHom T
14 13 eleq2d ⊢ S ∈ Grp ∧ X ∈ SubGrp ⁡ T ∧ ran ⁡ F ⊆ X → F ∈ S GrpHom T ↔ F ∈ S MndHom T
15 1 subggrp ⊢ X ∈ SubGrp ⁡ T → U ∈ Grp
16 15 adantr ⊢ X ∈ SubGrp ⁡ T ∧ ran ⁡ F ⊆ X → U ∈ Grp
17 ghmmhmb ⊢ S ∈ Grp ∧ U ∈ Grp → S GrpHom U = S MndHom U
18 16 17 sylan2 ⊢ S ∈ Grp ∧ X ∈ SubGrp ⁡ T ∧ ran ⁡ F ⊆ X → S GrpHom U = S MndHom U
19 18 eleq2d ⊢ S ∈ Grp ∧ X ∈ SubGrp ⁡ T ∧ ran ⁡ F ⊆ X → F ∈ S GrpHom U ↔ F ∈ S MndHom U
20 9 14 19 3bitr4d ⊢ S ∈ Grp ∧ X ∈ SubGrp ⁡ T ∧ ran ⁡ F ⊆ X → F ∈ S GrpHom T ↔ F ∈ S GrpHom U
21 20 expcom ⊢ X ∈ SubGrp ⁡ T ∧ ran ⁡ F ⊆ X → S ∈ Grp → F ∈ S GrpHom T ↔ F ∈ S GrpHom U
22 3 5 21 pm5.21ndd ⊢ X ∈ SubGrp ⁡ T ∧ ran ⁡ F ⊆ X → F ∈ S GrpHom T ↔ F ∈ S GrpHom U