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

Metamath Proof Explorer

Theorem rnghmrcl

Description: Reverse closure of a non-unital ring homomorphism. (Contributed by AV, 22-Feb-2020)

		Ref	Expression
	Assertion	rnghmrcl	$⊢ F \in (R RngHom S) \to (R \in Rng \land S \in Rng)$

Step	Hyp	Ref	Expression
1		df-rnghm	$⊢ RngHom = (r \in Rng, s \in Rng ⟼ ⦋ {Base}_{r} / v ⦌ ⦋ {Base}_{s} / w ⦌ \{f \in (w^{v}) \| \forall x \in v \forall y \in v (f (x +_{r} y) = f (x) +_{s} f (y) \land f (x \cdot_{r} y) = f (x) \cdot_{s} f (y))\})$
2	1	elmpocl	$⊢ F \in (R RngHom S) \to (R \in Rng \land S \in Rng)$