# Metamath Proof Explorer

## 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}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{S}}\phantom{\rule{.4em}{0ex}}{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}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{S}}\phantom{\rule{.4em}{0ex}}{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)↔\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}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{S}}\phantom{\rule{.4em}{0ex}}{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)$