Theorem c0snghm

Description: The constant mapping to zero is a group homomorphism from the trivial group (consisting of the zero only) to any group. (Contributed by AV, 17-Apr-2020)

	Ref	Expression
Hypotheses	zrrhm.b	⊢ 𝐵 = ( Base ‘ 𝑇 )
	zrrhm.0	⊢ 0 = ( 0g ‘ 𝑆 )
	zrrhm.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 ↦ 0 )
	c0snmhm.z	⊢ 𝑍 = ( 0g ‘ 𝑇 )
Assertion	c0snghm	⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ∧ 𝐵 = { 𝑍 } ) → 𝐻 ∈ ( 𝑇 GrpHom 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		zrrhm.b	⊢ 𝐵 = ( Base ‘ 𝑇 )
2		zrrhm.0	⊢ 0 = ( 0g ‘ 𝑆 )
3		zrrhm.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 ↦ 0 )
4		c0snmhm.z	⊢ 𝑍 = ( 0g ‘ 𝑇 )
5		grpmnd	⊢ ( 𝑆 ∈ Grp → 𝑆 ∈ Mnd )
6		grpmnd	⊢ ( 𝑇 ∈ Grp → 𝑇 ∈ Mnd )
7		id	⊢ ( 𝐵 = { 𝑍 } → 𝐵 = { 𝑍 } )
8	1 2 3 4	c0snmhm	⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ∧ 𝐵 = { 𝑍 } ) → 𝐻 ∈ ( 𝑇 MndHom 𝑆 ) )
9	5 6 7 8	syl3an	⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ∧ 𝐵 = { 𝑍 } ) → 𝐻 ∈ ( 𝑇 MndHom 𝑆 ) )
10		ghmmhmb	⊢ ( ( 𝑇 ∈ Grp ∧ 𝑆 ∈ Grp ) → ( 𝑇 GrpHom 𝑆 ) = ( 𝑇 MndHom 𝑆 ) )
11	10	eleq2d	⊢ ( ( 𝑇 ∈ Grp ∧ 𝑆 ∈ Grp ) → ( 𝐻 ∈ ( 𝑇 GrpHom 𝑆 ) ↔ 𝐻 ∈ ( 𝑇 MndHom 𝑆 ) ) )
12	11	ancoms	⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝐻 ∈ ( 𝑇 GrpHom 𝑆 ) ↔ 𝐻 ∈ ( 𝑇 MndHom 𝑆 ) ) )
13	12	3adant3	⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ∧ 𝐵 = { 𝑍 } ) → ( 𝐻 ∈ ( 𝑇 GrpHom 𝑆 ) ↔ 𝐻 ∈ ( 𝑇 MndHom 𝑆 ) ) )
14	9 13	mpbird	⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ∧ 𝐵 = { 𝑍 } ) → 𝐻 ∈ ( 𝑇 GrpHom 𝑆 ) )