Metamath Proof Explorer


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 )