Theorem ghmmhm

Description: A group homomorphism is a monoid homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015)

	Ref	Expression
Assertion	ghmmhm	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to F\in \left(S\mathrm{MndHom}T\right)$$

Proof

Step	Hyp	Ref	Expression
1		ghmgrp1	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to S\in \mathrm{Grp}$$
2		grpmnd	$$⊢S\in \mathrm{Grp}\to S\in \mathrm{Mnd}$$
3	1 2	syl	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to S\in \mathrm{Mnd}$$
4		ghmgrp2	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to T\in \mathrm{Grp}$$
5		grpmnd	$$⊢T\in \mathrm{Grp}\to T\in \mathrm{Mnd}$$
6	4 5	syl	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to T\in \mathrm{Mnd}$$
7		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
8		eqid	$$⊢{\mathrm{Base}}_T={\mathrm{Base}}_T$$
9	7 8	ghmf	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to F:{\mathrm{Base}}_S⟶{\mathrm{Base}}_T$$
10		eqid	$$⊢{+}_S={+}_S$$
11		eqid	$$⊢{+}_T={+}_T$$
12	7 10 11	ghmlin	$$⊢\left(F\in \left(S\mathrm{GrpHom}T\right)\wedge x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to F\left(x{+}_{S}y\right)=F\left(x\right){+}_{T}F\left(y\right)$$
13	12	3expb	$$⊢\left(F\in \left(S\mathrm{GrpHom}T\right)\wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\right)\to F\left(x{+}_{S}y\right)=F\left(x\right){+}_{T}F\left(y\right)$$
14	13	ralrimivva	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to \forall x\in {\mathrm{Base}}_S\forall y\in {\mathrm{Base}}_{S}F\left(x{+}_{S}y\right)=F\left(x\right){+}_{T}F\left(y\right)$$
15		eqid	$$⊢0_S=0_S$$
16		eqid	$$⊢0_T=0_T$$
17	15 16	ghmid	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to F\left(0_S\right)=0_T$$
18	9 14 17	3jca	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to \left(F:{\mathrm{Base}}_S⟶{\mathrm{Base}}_T\wedge \forall x\in {\mathrm{Base}}_S\forall y\in {\mathrm{Base}}_{S}F\left(x{+}_{S}y\right)=F\left(x\right){+}_{T}F\left(y\right)\wedge F\left(0_S\right)=0_T\right)$$
19	7 8 10 11 15 16	ismhm	$$⊢F\in \left(S\mathrm{MndHom}T\right)\leftrightarrow \left(\left(S\in \mathrm{Mnd}\wedge T\in \mathrm{Mnd}\right)\wedge \left(F:{\mathrm{Base}}_S⟶{\mathrm{Base}}_T\wedge \forall x\in {\mathrm{Base}}_S\forall y\in {\mathrm{Base}}_{S}F\left(x{+}_{S}y\right)=F\left(x\right){+}_{T}F\left(y\right)\wedge F\left(0_S\right)=0_T\right)\right)$$
20	3 6 18 19	syl21anbrc	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to F\in \left(S\mathrm{MndHom}T\right)$$