Theorem ricsym

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

	Ref	Expression
Assertion	ricsym	|- ( R ~=r S -> S ~=r R )

Proof

Step	Hyp	Ref	Expression
1		brric	|- ( R ~=r S <-> ( R RingIso S ) =/= (/) )
2		n0	|- ( ( R RingIso S ) =/= (/) <-> E. f f e. ( R RingIso S ) )
3		rimcnv	|- ( f e. ( R RingIso S ) -> `' f e. ( S RingIso R ) )
4		brrici	|- ( `' f e. ( S RingIso R ) -> S ~=r R )
5	3 4	syl	|- ( f e. ( R RingIso S ) -> S ~=r R )
6	5	exlimiv	|- ( E. f f e. ( R RingIso S ) -> S ~=r R )
7	2 6	sylbi	|- ( ( R RingIso S ) =/= (/) -> S ~=r R )
8	1 7	sylbi	|- ( R ~=r S -> S ~=r R )