Theorem riclcl

Description: Ring isomorphism implies the left side is a ring. (Contributed by AV, 23-Jul-2026)

	Ref	Expression
Assertion	riclcl	⊢ ( 𝑅 ≃𝑟 𝑆 → 𝑅 ∈ Ring )

Proof

Step	Hyp	Ref	Expression
1		brric	⊢ ( 𝑅 ≃𝑟 𝑆 ↔ ( 𝑅 RingIso 𝑆 ) ≠ ∅ )
2		n0	⊢ ( ( 𝑅 RingIso 𝑆 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) )
3	1 2	bitri	⊢ ( 𝑅 ≃𝑟 𝑆 ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) )
4		rimrcl1	⊢ ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → 𝑅 ∈ Ring )
5	4	exlimiv	⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → 𝑅 ∈ Ring )
6	3 5	sylbi	⊢ ( 𝑅 ≃𝑟 𝑆 → 𝑅 ∈ Ring )