ghmima

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

		Ref	Expression
	Assertion	ghmima	$⊢ (F \in (S GrpHom T) \land U \in SubGrp (S)) \to F [U] \in SubGrp (T)$

Step	Hyp	Ref	Expression
1		df-ima	$⊢ F [U] = ran ({F ↾}_{U})$
2		eqid	$⊢ S ↾_{𝑠} U = S ↾_{𝑠} U$
3	2	resghm	$⊢ (F \in (S GrpHom T) \land U \in SubGrp (S)) \to {F ↾}_{U} \in ((S ↾_{𝑠} U) GrpHom T)$
4		ghmrn	$⊢ {F ↾}_{U} \in ((S ↾_{𝑠} U) GrpHom T) \to ran ({F ↾}_{U}) \in SubGrp (T)$
5	3 4	syl	$⊢ (F \in (S GrpHom T) \land U \in SubGrp (S)) \to ran ({F ↾}_{U}) \in SubGrp (T)$
6	1 5	eqeltrid	$⊢ (F \in (S GrpHom T) \land U \in SubGrp (S)) \to F [U] \in SubGrp (T)$

Metamath Proof Explorer