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 e. ( S RngIso T ) -> `' F e. ( T RngIso S ) )

Proof

Step Hyp Ref Expression
1 rngimrcl 
 |-  ( F e. ( S RngIso T ) -> ( S e. _V /\ T e. _V ) )
2 isrngim 
 |-  ( ( S e. _V /\ T e. _V ) -> ( F e. ( S RngIso T ) <-> ( F e. ( S RngHom T ) /\ `' F e. ( T RngHom S ) ) ) )
3 eqid 
 |-  ( Base ` S ) = ( Base ` S )
4 eqid 
 |-  ( Base ` T ) = ( Base ` T )
5 3 4 rnghmf 
 |-  ( F e. ( S RngHom T ) -> F : ( Base ` S ) --> ( Base ` T ) )
6 frel 
 |-  ( F : ( Base ` S ) --> ( Base ` T ) -> Rel F )
7 dfrel2 
 |-  ( Rel F <-> `' `' F = F )
8 6 7 sylib 
 |-  ( F : ( Base ` S ) --> ( Base ` T ) -> `' `' F = F )
9 5 8 syl 
 |-  ( F e. ( S RngHom T ) -> `' `' F = F )
10 id 
 |-  ( F e. ( S RngHom T ) -> F e. ( S RngHom T ) )
11 9 10 eqeltrd 
 |-  ( F e. ( S RngHom T ) -> `' `' F e. ( S RngHom T ) )
12 11 anim1ci 
 |-  ( ( F e. ( S RngHom T ) /\ `' F e. ( T RngHom S ) ) -> ( `' F e. ( T RngHom S ) /\ `' `' F e. ( S RngHom T ) ) )
13 isrngim 
 |-  ( ( T e. _V /\ S e. _V ) -> ( `' F e. ( T RngIso S ) <-> ( `' F e. ( T RngHom S ) /\ `' `' F e. ( S RngHom T ) ) ) )
14 13 ancoms 
 |-  ( ( S e. _V /\ T e. _V ) -> ( `' F e. ( T RngIso S ) <-> ( `' F e. ( T RngHom S ) /\ `' `' F e. ( S RngHom T ) ) ) )
15 12 14 imbitrrid 
 |-  ( ( S e. _V /\ T e. _V ) -> ( ( F e. ( S RngHom T ) /\ `' F e. ( T RngHom S ) ) -> `' F e. ( T RngIso S ) ) )
16 2 15 sylbid 
 |-  ( ( S e. _V /\ T e. _V ) -> ( F e. ( S RngIso T ) -> `' F e. ( T RngIso S ) ) )
17 1 16 mpcom 
 |-  ( F e. ( S RngIso T ) -> `' F e. ( T RngIso S ) )