Metamath Proof Explorer

Theorem rimisrngim

Description: Each unital ring isomorphism is a non-unital ring isomorphism. (Contributed by AV, 30-Mar-2025)

Ref Expression
Assertion rimisrngim 
|- ( F e. ( R RingIso S ) -> F e. ( R RngIso S ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` R ) = ( Base ` R )
2 eqid 
 |-  ( Base ` S ) = ( Base ` S )
3 1 2 isrim 
 |-  ( F e. ( R RingIso S ) <-> ( F e. ( R RingHom S ) /\ F : ( Base ` R ) -1-1-onto-> ( Base ` S ) ) )
4 rhmisrnghm 
 |-  ( F e. ( R RingHom S ) -> F e. ( R RngHom S ) )
5 4 anim1i 
 |-  ( ( F e. ( R RingHom S ) /\ F : ( Base ` R ) -1-1-onto-> ( Base ` S ) ) -> ( F e. ( R RngHom S ) /\ F : ( Base ` R ) -1-1-onto-> ( Base ` S ) ) )
6 3 5 sylbi 
 |-  ( F e. ( R RingIso S ) -> ( F e. ( R RngHom S ) /\ F : ( Base ` R ) -1-1-onto-> ( Base ` S ) ) )
7 rimrcl 
 |-  ( F e. ( R RingIso S ) -> ( R e. _V /\ S e. _V ) )
8 1 2 isrngim2 
 |-  ( ( R e. _V /\ S e. _V ) -> ( F e. ( R RngIso S ) <-> ( F e. ( R RngHom S ) /\ F : ( Base ` R ) -1-1-onto-> ( Base ` S ) ) ) )
9 7 8 syl 
 |-  ( F e. ( R RingIso S ) -> ( F e. ( R RngIso S ) <-> ( F e. ( R RngHom S ) /\ F : ( Base ` R ) -1-1-onto-> ( Base ` S ) ) ) )
10 6 9 mpbird 
 |-  ( F e. ( R RingIso S ) -> F e. ( R RngIso S ) )