Theorem ghmghmrn

Description: A group homomorphism from G to H is also a group homomorphism from G to its image in H . (Contributed by Paul Chapman, 3-Mar-2008) (Revised by AV, 26-Aug-2021)

	Ref	Expression
Hypothesis	ghmghmrn.u	⊢ 𝑈 = ( 𝑇 ↾s ran 𝐹 )
Assertion	ghmghmrn	⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		ghmghmrn.u	⊢ 𝑈 = ( 𝑇 ↾s ran 𝐹 )
2		ghmrn	⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ran 𝐹 ∈ ( SubGrp ‘ 𝑇 ) )
3		ssid	⊢ ran 𝐹 ⊆ ran 𝐹
4	1	resghm2b	⊢ ( ( ran 𝐹 ∈ ( SubGrp ‘ 𝑇 ) ∧ ran 𝐹 ⊆ ran 𝐹 ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) ) )
5	3 4	mpan2	⊢ ( ran 𝐹 ∈ ( SubGrp ‘ 𝑇 ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) ) )
6	5	biimpd	⊢ ( ran 𝐹 ∈ ( SubGrp ‘ 𝑇 ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) ) )
7	2 6	mpcom	⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) )