Metamath Proof Explorer

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

Proof

Step	Hyp	Ref	Expression
1		zrrhm.b	$⊢ B = {Base}_{T}$
2		zrrhm.0	$⊢ \underset{˙}{0} = 0_{S}$
3		zrrhm.h	$⊢ H = (x \in B ⟼ \underset{˙}{0})$
4		c0snmhm.z	$⊢ Z = 0_{T}$
5		grpmnd	$⊢ S \in Grp \to S \in Mnd$
6		grpmnd	$⊢ T \in Grp \to T \in Mnd$
7		id	$⊢ B = \{Z\} \to B = \{Z\}$
8	1 2 3 4	c0snmhm	$⊢ (S \in Mnd \land T \in Mnd \land B = \{Z\}) \to H \in (T MndHom S)$
9	5 6 7 8	syl3an	$⊢ (S \in Grp \land T \in Grp \land B = \{Z\}) \to H \in (T MndHom S)$
10		ghmmhmb	$⊢ (T \in Grp \land S \in Grp) \to T GrpHom S = T MndHom S$
11	10	eleq2d	$⊢ (T \in Grp \land S \in Grp) \to (H \in (T GrpHom S) \leftrightarrow H \in (T MndHom S))$
12	11	ancoms	$⊢ (S \in Grp \land T \in Grp) \to (H \in (T GrpHom S) \leftrightarrow H \in (T MndHom S))$
13	12	3adant3	$⊢ (S \in Grp \land T \in Grp \land B = \{Z\}) \to (H \in (T GrpHom S) \leftrightarrow H \in (T MndHom S))$
14	9 13	mpbird	$⊢ (S \in Grp \land T \in Grp \land B = \{Z\}) \to H \in (T GrpHom S)$