Metamath Proof Explorer

Theorem rimrcl1

Description: Reverse closure of a ring isomorphism. (Contributed by SN, 19-Feb-2025)

		Ref	Expression
	Assertion	rimrcl1	$⊢ F \in (R RingIso S) \to R \in Ring$

Step	Hyp	Ref	Expression
1		rimrhm	$⊢ F \in (R RingIso S) \to F \in (R RingHom S)$
2		rhmrcl1	$⊢ F \in (R RingHom S) \to R \in Ring$
3	1 2	syl	$⊢ F \in (R RingIso S) \to R \in Ring$