Metamath Proof Explorer

Theorem ghmima

Description: The image of a subgroup under a homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014)

Ref Expression
Assertion ghmima ⊢ F ∈ S GrpHom T ∧ U ∈ SubGrp ⁡ S → F U ∈ SubGrp ⁡ T

Proof

Step Hyp Ref Expression
1 df-ima ⊢ F U = ran ⁡ F ↾ U
2 eqid ⊢ S ↾ 𝑠 U = S ↾ 𝑠 U
3 2 resghm ⊢ F ∈ S GrpHom T ∧ U ∈ SubGrp ⁡ S → F ↾ U ∈ S ↾ 𝑠 U GrpHom T
4 ghmrn ⊢ F ↾ U ∈ S ↾ 𝑠 U GrpHom T → ran ⁡ F ↾ U ∈ SubGrp ⁡ T
5 3 4 syl ⊢ F ∈ S GrpHom T ∧ U ∈ SubGrp ⁡ S → ran ⁡ F ↾ U ∈ SubGrp ⁡ T
6 1 5 eqeltrid ⊢ F ∈ S GrpHom T ∧ U ∈ SubGrp ⁡ S → F U ∈ SubGrp ⁡ T