Theorem rnghmrcl

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

	Ref	Expression
Assertion	rnghmrcl	$$⊢F\in \left(R\mathrm{RngHomo}S\right)\to \left(R\in \mathrm{Rng}\wedge S\in \mathrm{Rng}\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-rnghomo	$$⊢\mathrm{RngHomo}=\left(r\in \mathrm{Rng},s\in \mathrm{Rng}⟼⦋{\mathrm{Base}}_r/v⦌⦋{\mathrm{Base}}_s/w⦌\left\{f\in \left(w^v\right)|\forall x\in v\forall y\in v\left(f\left(x{+}_{r}y\right)=f\left(x\right){+}_{s}f\left(y\right)\wedge f\left(x{\cdot }_{r}y\right)=f\left(x\right){\cdot }_{s}f\left(y\right)\right)\right\}\right)$$
2	1	elmpocl	$$⊢F\in \left(R\mathrm{RngHomo}S\right)\to \left(R\in \mathrm{Rng}\wedge S\in \mathrm{Rng}\right)$$