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	|- B = ( Base ` T )
	zrrhm.0	|- .0. = ( 0g ` S )
	zrrhm.h	|- H = ( x e. B |-> .0. )
	c0snmhm.z	|- Z = ( 0g ` T )
Assertion	c0snghm	|- ( ( S e. Grp /\ T e. Grp /\ B = { Z } ) -> H e. ( T GrpHom S ) )

Proof

Step	Hyp	Ref	Expression
1		zrrhm.b	|- B = ( Base ` T )
2		zrrhm.0	|- .0. = ( 0g ` S )
3		zrrhm.h	|- H = ( x e. B |-> .0. )
4		c0snmhm.z	|- Z = ( 0g ` T )
5		grpmnd	|- ( S e. Grp -> S e. Mnd )
6		grpmnd	|- ( T e. Grp -> T e. Mnd )
7		id	|- ( B = { Z } -> B = { Z } )
8	1 2 3 4	c0snmhm	|- ( ( S e. Mnd /\ T e. Mnd /\ B = { Z } ) -> H e. ( T MndHom S ) )
9	5 6 7 8	syl3an	|- ( ( S e. Grp /\ T e. Grp /\ B = { Z } ) -> H e. ( T MndHom S ) )
10		ghmmhmb	|- ( ( T e. Grp /\ S e. Grp ) -> ( T GrpHom S ) = ( T MndHom S ) )
11	10	eleq2d	|- ( ( T e. Grp /\ S e. Grp ) -> ( H e. ( T GrpHom S ) <-> H e. ( T MndHom S ) ) )
12	11	ancoms	|- ( ( S e. Grp /\ T e. Grp ) -> ( H e. ( T GrpHom S ) <-> H e. ( T MndHom S ) ) )
13	12	3adant3	|- ( ( S e. Grp /\ T e. Grp /\ B = { Z } ) -> ( H e. ( T GrpHom S ) <-> H e. ( T MndHom S ) ) )
14	9 13	mpbird	|- ( ( S e. Grp /\ T e. Grp /\ B = { Z } ) -> H e. ( T GrpHom S ) )