Metamath Proof Explorer


Theorem rimrcl2

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

Ref Expression
Assertion rimrcl2 F R RingIso S S Ring

Proof

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