Theorem ghmima

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

	Ref	Expression
Assertion	ghmima	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑆 ) ) → ( 𝐹 “ 𝑈 ) ∈ ( SubGrp ‘ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		df-ima	⊢ ( 𝐹 “ 𝑈 ) = ran ( 𝐹 ↾ 𝑈 )
2		eqid	⊢ ( 𝑆 ↾s 𝑈 ) = ( 𝑆 ↾s 𝑈 )
3	2	resghm	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑆 ) ) → ( 𝐹 ↾ 𝑈 ) ∈ ( ( 𝑆 ↾s 𝑈 ) GrpHom 𝑇 ) )
4		ghmrn	⊢ ( ( 𝐹 ↾ 𝑈 ) ∈ ( ( 𝑆 ↾s 𝑈 ) GrpHom 𝑇 ) → ran ( 𝐹 ↾ 𝑈 ) ∈ ( SubGrp ‘ 𝑇 ) )
5	3 4	syl	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑆 ) ) → ran ( 𝐹 ↾ 𝑈 ) ∈ ( SubGrp ‘ 𝑇 ) )
6	1 5	eqeltrid	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑆 ) ) → ( 𝐹 “ 𝑈 ) ∈ ( SubGrp ‘ 𝑇 ) )