Metamath Proof Explorer


Theorem rimrcl1

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

Ref Expression
Assertion rimrcl1 F R RingIso S R Ring

Proof

Step Hyp Ref Expression
1 rimrhm F R RingIso S F R RingHom S
2 rhmrcl1 F R RingHom S R Ring
3 1 2 syl F R RingIso S R Ring