This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mgmhmrcl

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

		Ref	Expression
	Assertion	mgmhmrcl	$⊢ F \in (S MgmHom T) \to (S \in Mgm \land T \in Mgm)$

Step	Hyp	Ref	Expression
1		df-mgmhm	$⊢ MgmHom = (s \in Mgm, t \in Mgm ⟼ \{f \in ({Base}_{t}^{{Base}_{s}}) \| \forall x \in {Base}_{s} \forall y \in {Base}_{s} f (x +_{s} y) = f (x) +_{t} f (y)\})$
2	1	elmpocl	$⊢ F \in (S MgmHom T) \to (S \in Mgm \land T \in Mgm)$