This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rngimcnv

Description: The converse of an isomorphism of non-unital rings is an isomorphism of non-unital rings. (Contributed by AV, 27-Feb-2025)

Ref Expression
Assertion rngimcnv ⊢ F ∈ S RngIso T → F -1 ∈ T RngIso S

Proof

Step Hyp Ref Expression
1 rngimrcl ⊢ F ∈ S RngIso T → S ∈ V ∧ T ∈ V
2 isrngim ⊢ S ∈ V ∧ T ∈ V → F ∈ S RngIso T ↔ F ∈ S RngHom T ∧ F -1 ∈ T RngHom S
3 eqid ⊢ Base S = Base S
4 eqid ⊢ Base T = Base T
5 3 4 rnghmf ⊢ F ∈ S RngHom T → F : Base S ⟶ Base T
6 frel ⊢ F : Base S ⟶ Base T → Rel ⁡ F
7 dfrel2 ⊢ Rel ⁡ F ↔ F -1 -1 = F
8 6 7 sylib ⊢ F : Base S ⟶ Base T → F -1 -1 = F
9 5 8 syl ⊢ F ∈ S RngHom T → F -1 -1 = F
10 id ⊢ F ∈ S RngHom T → F ∈ S RngHom T
11 9 10 eqeltrd ⊢ F ∈ S RngHom T → F -1 -1 ∈ S RngHom T
12 11 anim1ci ⊢ F ∈ S RngHom T ∧ F -1 ∈ T RngHom S → F -1 ∈ T RngHom S ∧ F -1 -1 ∈ S RngHom T
13 isrngim ⊢ T ∈ V ∧ S ∈ V → F -1 ∈ T RngIso S ↔ F -1 ∈ T RngHom S ∧ F -1 -1 ∈ S RngHom T
14 13 ancoms ⊢ S ∈ V ∧ T ∈ V → F -1 ∈ T RngIso S ↔ F -1 ∈ T RngHom S ∧ F -1 -1 ∈ S RngHom T
15 12 14 imbitrrid ⊢ S ∈ V ∧ T ∈ V → F ∈ S RngHom T ∧ F -1 ∈ T RngHom S → F -1 ∈ T RngIso S
16 2 15 sylbid ⊢ S ∈ V ∧ T ∈ V → F ∈ S RngIso T → F -1 ∈ T RngIso S
17 1 16 mpcom ⊢ F ∈ S RngIso T → F -1 ∈ T RngIso S