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

Metamath Proof Explorer

Theorem rhmrcl1

Description: Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015)

		Ref	Expression
	Assertion	rhmrcl1	$⊢ F \in (R RingHom S) \to R \in Ring$

Step	Hyp	Ref	Expression
1		dfrhm2	$⊢ RingHom = (r \in Ring, s \in Ring ⟼ (r GrpHom s) \cap ({mulGrp}_{r} MndHom {mulGrp}_{s}))$
2	1	elmpocl1	$⊢ F \in (R RingHom S) \to R \in Ring$