Theorem c0ghm

Description: The constant mapping to zero is a group homomorphism. (Contributed by AV, 16-Apr-2020)

	Ref	Expression
Hypotheses	c0mhm.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	c0mhm.0	⊢ 0 = ( 0g ‘ 𝑇 )
	c0mhm.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 ↦ 0 )
Assertion	c0ghm	⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → 𝐻 ∈ ( 𝑆 GrpHom 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		c0mhm.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
2		c0mhm.0	⊢ 0 = ( 0g ‘ 𝑇 )
3		c0mhm.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 ↦ 0 )
4		grpmnd	⊢ ( 𝑆 ∈ Grp → 𝑆 ∈ Mnd )
5		grpmnd	⊢ ( 𝑇 ∈ Grp → 𝑇 ∈ Mnd )
6	4 5	anim12i	⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) )
7	1 2 3	c0mhm	⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) → 𝐻 ∈ ( 𝑆 MndHom 𝑇 ) )
8	6 7	syl	⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → 𝐻 ∈ ( 𝑆 MndHom 𝑇 ) )
9		ghmmhmb	⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝑆 GrpHom 𝑇 ) = ( 𝑆 MndHom 𝑇 ) )
10	9	eleq2d	⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝐻 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ 𝐻 ∈ ( 𝑆 MndHom 𝑇 ) ) )
11	8 10	mpbird	⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → 𝐻 ∈ ( 𝑆 GrpHom 𝑇 ) )