Theorem mgmhmrcl

Description: Reverse closure of a magma homomorphism. (Contributed by AV, 24-Feb-2020)

	Ref	Expression
Assertion	mgmhmrcl	$$⊢F\in \left(S\mathrm{MgmHom}T\right)\to \left(S\in \mathrm{Mgm}\wedge T\in \mathrm{Mgm}\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-mgmhm	$$⊢\mathrm{MgmHom}=\left(s\in \mathrm{Mgm},t\in \mathrm{Mgm}⟼\left\{f\in \left({{\mathrm{Base}}_t}^{{\mathrm{Base}}_s}\right)|\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)\right\}\right)$$
2	1	elmpocl	$$⊢F\in \left(S\mathrm{MgmHom}T\right)\to \left(S\in \mathrm{Mgm}\wedge T\in \mathrm{Mgm}\right)$$