Metamath Proof Explorer


Theorem isrngim

Description: An isomorphism of non-unital rings is a bijective homomorphism. (Contributed by AV, 23-Feb-2020)

Ref Expression
Hypotheses rnghmf1o.b
|- B = ( Base ` R )
rnghmf1o.c
|- C = ( Base ` S )
Assertion isrngim
|- ( ( R e. V /\ S e. W ) -> ( F e. ( R RngIsom S ) <-> ( F e. ( R RngHomo S ) /\ F : B -1-1-onto-> C ) ) )

Proof

Step Hyp Ref Expression
1 rnghmf1o.b
 |-  B = ( Base ` R )
2 rnghmf1o.c
 |-  C = ( Base ` S )
3 isrngisom
 |-  ( ( R e. V /\ S e. W ) -> ( F e. ( R RngIsom S ) <-> ( F e. ( R RngHomo S ) /\ `' F e. ( S RngHomo R ) ) ) )
4 1 2 rnghmf1o
 |-  ( F e. ( R RngHomo S ) -> ( F : B -1-1-onto-> C <-> `' F e. ( S RngHomo R ) ) )
5 4 bicomd
 |-  ( F e. ( R RngHomo S ) -> ( `' F e. ( S RngHomo R ) <-> F : B -1-1-onto-> C ) )
6 5 a1i
 |-  ( ( R e. V /\ S e. W ) -> ( F e. ( R RngHomo S ) -> ( `' F e. ( S RngHomo R ) <-> F : B -1-1-onto-> C ) ) )
7 6 pm5.32d
 |-  ( ( R e. V /\ S e. W ) -> ( ( F e. ( R RngHomo S ) /\ `' F e. ( S RngHomo R ) ) <-> ( F e. ( R RngHomo S ) /\ F : B -1-1-onto-> C ) ) )
8 3 7 bitrd
 |-  ( ( R e. V /\ S e. W ) -> ( F e. ( R RngIsom S ) <-> ( F e. ( R RngHomo S ) /\ F : B -1-1-onto-> C ) ) )