Theorem rimrcl1

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

	Ref	Expression
Assertion	rimrcl1	$$⊢F\in \left(R\mathrm{RingIso}S\right)\to R\in \mathrm{Ring}$$

Proof

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