# Metamath Proof Explorer

## Theorem mgmhmf

Description: A magma homomorphism is a function. (Contributed by AV, 25-Feb-2020)

Ref Expression
Hypotheses mgmhmf.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
mgmhmf.c ${⊢}{C}={\mathrm{Base}}_{{T}}$
Assertion mgmhmf ${⊢}{F}\in \left({S}\mathrm{MgmHom}{T}\right)\to {F}:{B}⟶{C}$

### Proof

Step Hyp Ref Expression
1 mgmhmf.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
2 mgmhmf.c ${⊢}{C}={\mathrm{Base}}_{{T}}$
3 eqid ${⊢}{+}_{{S}}={+}_{{S}}$
4 eqid ${⊢}{+}_{{T}}={+}_{{T}}$
5 1 2 3 4 ismgmhm ${⊢}{F}\in \left({S}\mathrm{MgmHom}{T}\right)↔\left(\left({S}\in \mathrm{Mgm}\wedge {T}\in \mathrm{Mgm}\right)\wedge \left({F}:{B}⟶{C}\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({x}{+}_{{S}}{y}\right)={F}\left({x}\right){+}_{{T}}{F}\left({y}\right)\right)\right)$
6 simprl ${⊢}\left(\left({S}\in \mathrm{Mgm}\wedge {T}\in \mathrm{Mgm}\right)\wedge \left({F}:{B}⟶{C}\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({x}{+}_{{S}}{y}\right)={F}\left({x}\right){+}_{{T}}{F}\left({y}\right)\right)\right)\to {F}:{B}⟶{C}$
7 5 6 sylbi ${⊢}{F}\in \left({S}\mathrm{MgmHom}{T}\right)\to {F}:{B}⟶{C}$