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

Metamath Proof Explorer

Theorem isrngim

Description: An isomorphism of non-unital rings is a homomorphism whose converse is also a homomorphism. (Contributed by AV, 22-Feb-2020)

Ref Expression
Assertion isrngim 
|- ( ( R e. V /\ S e. W ) -> ( F e. ( R RngIso S ) <-> ( F e. ( R RngHom S ) /\ `' F e. ( S RngHom R ) ) ) )

Proof

Step Hyp Ref Expression
1 df-rngim 
 |-  RngIso = ( r e. _V , s e. _V |-> { f e. ( r RngHom s ) | `' f e. ( s RngHom r ) } )
2 1 a1i 
 |-  ( ( R e. V /\ S e. W ) -> RngIso = ( r e. _V , s e. _V |-> { f e. ( r RngHom s ) | `' f e. ( s RngHom r ) } ) )
3 oveq12 
 |-  ( ( r = R /\ s = S ) -> ( r RngHom s ) = ( R RngHom S ) )
4 3 adantl 
 |-  ( ( ( R e. V /\ S e. W ) /\ ( r = R /\ s = S ) ) -> ( r RngHom s ) = ( R RngHom S ) )
5 oveq12 
 |-  ( ( s = S /\ r = R ) -> ( s RngHom r ) = ( S RngHom R ) )
6 5 ancoms 
 |-  ( ( r = R /\ s = S ) -> ( s RngHom r ) = ( S RngHom R ) )
7 6 adantl 
 |-  ( ( ( R e. V /\ S e. W ) /\ ( r = R /\ s = S ) ) -> ( s RngHom r ) = ( S RngHom R ) )
8 7 eleq2d 
 |-  ( ( ( R e. V /\ S e. W ) /\ ( r = R /\ s = S ) ) -> ( `' f e. ( s RngHom r ) <-> `' f e. ( S RngHom R ) ) )
9 4 8 rabeqbidv 
 |-  ( ( ( R e. V /\ S e. W ) /\ ( r = R /\ s = S ) ) -> { f e. ( r RngHom s ) | `' f e. ( s RngHom r ) } = { f e. ( R RngHom S ) | `' f e. ( S RngHom R ) } )
10 elex 
 |-  ( R e. V -> R e. _V )
11 10 adantr 
 |-  ( ( R e. V /\ S e. W ) -> R e. _V )
12 elex 
 |-  ( S e. W -> S e. _V )
13 12 adantl 
 |-  ( ( R e. V /\ S e. W ) -> S e. _V )
14 ovex 
 |-  ( R RngHom S ) e. _V
15 14 rabex 
 |-  { f e. ( R RngHom S ) | `' f e. ( S RngHom R ) } e. _V
16 15 a1i 
 |-  ( ( R e. V /\ S e. W ) -> { f e. ( R RngHom S ) | `' f e. ( S RngHom R ) } e. _V )
17 2 9 11 13 16 ovmpod 
 |-  ( ( R e. V /\ S e. W ) -> ( R RngIso S ) = { f e. ( R RngHom S ) | `' f e. ( S RngHom R ) } )
18 17 eleq2d 
 |-  ( ( R e. V /\ S e. W ) -> ( F e. ( R RngIso S ) <-> F e. { f e. ( R RngHom S ) | `' f e. ( S RngHom R ) } ) )
19 cnveq 
 |-  ( f = F -> `' f = `' F )
20 19 eleq1d 
 |-  ( f = F -> ( `' f e. ( S RngHom R ) <-> `' F e. ( S RngHom R ) ) )
21 20 elrab 
 |-  ( F e. { f e. ( R RngHom S ) | `' f e. ( S RngHom R ) } <-> ( F e. ( R RngHom S ) /\ `' F e. ( S RngHom R ) ) )
22 18 21 bitrdi 
 |-  ( ( R e. V /\ S e. W ) -> ( F e. ( R RngIso S ) <-> ( F e. ( R RngHom S ) /\ `' F e. ( S RngHom R ) ) ) )