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	$⊢ \underset{˙}{0} = 0_{T}$
	c0mhm.h	$⊢ H = (x \in B ⟼ \underset{˙}{0})$
Assertion	c0ghm	$⊢ (S \in Grp \land T \in Grp) \to H \in (S GrpHom T)$

Step	Hyp	Ref	Expression
1		c0mhm.b	$⊢ B = {Base}_{S}$
2		c0mhm.0	$⊢ \underset{˙}{0} = 0_{T}$
3		c0mhm.h	$⊢ H = (x \in B ⟼ \underset{˙}{0})$
4		grpmnd	$⊢ S \in Grp \to S \in Mnd$
5		grpmnd	$⊢ T \in Grp \to T \in Mnd$
6	4 5	anim12i	$⊢ (S \in Grp \land T \in Grp) \to (S \in Mnd \land T \in Mnd)$
7	1 2 3	c0mhm	$⊢ (S \in Mnd \land T \in Mnd) \to H \in (S MndHom T)$
8	6 7	syl	$⊢ (S \in Grp \land T \in Grp) \to H \in (S MndHom T)$
9		ghmmhmb	$⊢ (S \in Grp \land T \in Grp) \to S GrpHom T = S MndHom T$
10	9	eleq2d	$⊢ (S \in Grp \land T \in Grp) \to (H \in (S GrpHom T) \leftrightarrow H \in (S MndHom T))$
11	8 10	mpbird	$⊢ (S \in Grp \land T \in Grp) \to H \in (S GrpHom T)$

Metamath Proof Explorer