Metamath Proof Explorer

Theorem rimcnv

Description: The converse of a ring isomorphism is a ring isomorphism. (Contributed by Jeff Madsen, 16-Jun-2011) (Revised 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