Metamath Proof Explorer


Theorem rimcnv

Description: The converse of a ring isomorphism is a ring isomorphism. (Contributed by SN, 10-Jan-2025)

Ref Expression
Assertion rimcnv F R RingIso S F -1 S RingIso R

Proof

Step Hyp Ref Expression
1 eqid Base R = Base R
2 eqid Base S = Base S
3 1 2 rhmf F R RingHom S F : Base R Base S
4 frel F : Base R Base S Rel F
5 dfrel2 Rel F F -1 -1 = F
6 4 5 sylib F : Base R Base S F -1 -1 = F
7 3 6 syl F R RingHom S F -1 -1 = F
8 id F R RingHom S F R RingHom S
9 7 8 eqeltrd F R RingHom S F -1 -1 R RingHom S
10 9 anim1ci F R RingHom S F -1 S RingHom R F -1 S RingHom R F -1 -1 R RingHom S
11 isrim0 F R RingIso S F R RingHom S F -1 S RingHom R
12 isrim0 F -1 S RingIso R F -1 S RingHom R F -1 -1 R RingHom S
13 10 11 12 3imtr4i F R RingIso S F -1 S RingIso R