Metamath Proof Explorer

Theorem ghmmhmb

Description: Group homomorphisms and monoid homomorphisms coincide. (Thus, GrpHom is somewhat redundant, although its stronger reverse closure properties are sometimes useful.) (Contributed by Stefan O'Rear, 7-Mar-2015)

		Ref	Expression
	Assertion	ghmmhmb	$⊢ (S \in Grp \land T \in Grp) \to S GrpHom T = S MndHom T$

Proof

Step	Hyp	Ref	Expression
1		ghmmhm	$⊢ f \in (S GrpHom T) \to f \in (S MndHom T)$
2		eqid	$⊢ {Base}_{S} = {Base}_{S}$
3		eqid	$⊢ {Base}_{T} = {Base}_{T}$
4		eqid	$⊢ +_{S} = +_{S}$
5		eqid	$⊢ +_{T} = +_{T}$
6		simpll	$⊢ ((S \in Grp \land T \in Grp) \land f \in (S MndHom T)) \to S \in Grp$
7		simplr	$⊢ ((S \in Grp \land T \in Grp) \land f \in (S MndHom T)) \to T \in Grp$
8	2 3	mhmf	$⊢ f \in (S MndHom T) \to f : {Base}_{S} ⟶ {Base}_{T}$
9	8	adantl	$⊢ ((S \in Grp \land T \in Grp) \land f \in (S MndHom T)) \to f : {Base}_{S} ⟶ {Base}_{T}$
10	2 4 5	mhmlin	$⊢ (f \in (S MndHom T) \land x \in {Base}_{S} \land y \in {Base}_{S}) \to f (x +_{S} y) = f (x) +_{T} f (y)$
11	10	3expb	$⊢ (f \in (S MndHom T) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to f (x +_{S} y) = f (x) +_{T} f (y)$
12	11	adantll	$⊢ (((S \in Grp \land T \in Grp) \land f \in (S MndHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to f (x +_{S} y) = f (x) +_{T} f (y)$
13	2 3 4 5 6 7 9 12	isghmd	$⊢ ((S \in Grp \land T \in Grp) \land f \in (S MndHom T)) \to f \in (S GrpHom T)$
14	13	ex	$⊢ (S \in Grp \land T \in Grp) \to (f \in (S MndHom T) \to f \in (S GrpHom T))$
15	1 14	impbid2	$⊢ (S \in Grp \land T \in Grp) \to (f \in (S GrpHom T) \leftrightarrow f \in (S MndHom T))$
16	15	eqrdv	$⊢ (S \in Grp \land T \in Grp) \to S GrpHom T = S MndHom T$