Metamath Proof Explorer


Theorem rimrcl1

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

Ref Expression
Assertion rimrcl1 ( 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) → 𝑅 ∈ Ring )

Proof

Step Hyp Ref Expression
1 rimrhm ( 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
2 rhmrcl1 ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ Ring )
3 1 2 syl ( 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) → 𝑅 ∈ Ring )