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

Metamath Proof Explorer

Theorem mhmrcl1

Description: Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015)

		Ref	Expression
	Assertion	mhmrcl1	$⊢ F \in (S MndHom T) \to S \in Mnd$

Step	Hyp	Ref	Expression
1		df-mhm	$⊢ MndHom = (s \in Mnd, t \in Mnd ⟼ \{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) \land f (0_{s}) = 0_{t})\})$
2	1	elmpocl1	$⊢ F \in (S MndHom T) \to S \in Mnd$