Theorem c0ghm

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

	Ref	Expression
Hypotheses	c0mhm.b	|- B = ( Base ` S )
	c0mhm.0	|- .0. = ( 0g ` T )
	c0mhm.h	|- H = ( x e. B |-> .0. )
Assertion	c0ghm	|- ( ( S e. Grp /\ T e. Grp ) -> H e. ( S GrpHom T ) )

Proof

Step	Hyp	Ref	Expression
1		c0mhm.b	|- B = ( Base ` S )
2		c0mhm.0	|- .0. = ( 0g ` T )
3		c0mhm.h	|- H = ( x e. B |-> .0. )
4		grpmnd	|- ( S e. Grp -> S e. Mnd )
5		grpmnd	|- ( T e. Grp -> T e. Mnd )
6	4 5	anim12i	|- ( ( S e. Grp /\ T e. Grp ) -> ( S e. Mnd /\ T e. Mnd ) )
7	1 2 3	c0mhm	|- ( ( S e. Mnd /\ T e. Mnd ) -> H e. ( S MndHom T ) )
8	6 7	syl	|- ( ( S e. Grp /\ T e. Grp ) -> H e. ( S MndHom T ) )
9		ghmmhmb	|- ( ( S e. Grp /\ T e. Grp ) -> ( S GrpHom T ) = ( S MndHom T ) )
10	9	eleq2d	|- ( ( S e. Grp /\ T e. Grp ) -> ( H e. ( S GrpHom T ) <-> H e. ( S MndHom T ) ) )
11	8 10	mpbird	|- ( ( S e. Grp /\ T e. Grp ) -> H e. ( S GrpHom T ) )