Theorem ricsym

Description: Ring isomorphism is symmetric. (Contributed by SN, 10-Jan-2025)

	Ref	Expression
Assertion	ricsym	⊢ ( 𝑅 ≃𝑟 𝑆 → 𝑆 ≃𝑟 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		brric	⊢ ( 𝑅 ≃𝑟 𝑆 ↔ ( 𝑅 RingIso 𝑆 ) ≠ ∅ )
2		n0	⊢ ( ( 𝑅 RingIso 𝑆 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) )
3		rimcnv	⊢ ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → ◡ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) )
4		brrici	⊢ ( ◡ 𝑓 ∈ ( 𝑆 RingIso 𝑅 ) → 𝑆 ≃𝑟 𝑅 )
5	3 4	syl	⊢ ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → 𝑆 ≃𝑟 𝑅 )
6	5	exlimiv	⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → 𝑆 ≃𝑟 𝑅 )
7	2 6	sylbi	⊢ ( ( 𝑅 RingIso 𝑆 ) ≠ ∅ → 𝑆 ≃𝑟 𝑅 )
8	1 7	sylbi	⊢ ( 𝑅 ≃𝑟 𝑆 → 𝑆 ≃𝑟 𝑅 )