Metamath Proof Explorer

Theorem isrim0

Description: A ring isomorphism is a homomorphism whose converse is also a homomorphism. Compare isgim2 . (Contributed by AV, 22-Oct-2019) Remove sethood antecedent. (Revised by SN, 10-Jan-2025)

Ref Expression
Assertion isrim0 
|- ( F e. ( R RingIso S ) <-> ( F e. ( R RingHom S ) /\ `' F e. ( S RingHom R ) ) )

Proof

Step Hyp Ref Expression
1 rimrcl 
 |-  ( F e. ( R RingIso S ) -> ( R e. _V /\ S e. _V ) )
2 rhmrcl1 
 |-  ( F e. ( R RingHom S ) -> R e. Ring )
3 2 elexd 
 |-  ( F e. ( R RingHom S ) -> R e. _V )
4 rhmrcl2 
 |-  ( F e. ( R RingHom S ) -> S e. Ring )
5 4 elexd 
 |-  ( F e. ( R RingHom S ) -> S e. _V )
6 3 5 jca 
 |-  ( F e. ( R RingHom S ) -> ( R e. _V /\ S e. _V ) )
7 6 adantr 
 |-  ( ( F e. ( R RingHom S ) /\ `' F e. ( S RingHom R ) ) -> ( R e. _V /\ S e. _V ) )
8 df-rim 
 |-  RingIso = ( r e. _V , s e. _V |-> { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } )
9 8 a1i 
 |-  ( ( R e. _V /\ S e. _V ) -> RingIso = ( r e. _V , s e. _V |-> { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } ) )
10 oveq12 
 |-  ( ( r = R /\ s = S ) -> ( r RingHom s ) = ( R RingHom S ) )
11 10 adantl 
 |-  ( ( ( R e. _V /\ S e. _V ) /\ ( r = R /\ s = S ) ) -> ( r RingHom s ) = ( R RingHom S ) )
12 oveq12 
 |-  ( ( s = S /\ r = R ) -> ( s RingHom r ) = ( S RingHom R ) )
13 12 ancoms 
 |-  ( ( r = R /\ s = S ) -> ( s RingHom r ) = ( S RingHom R ) )
14 13 adantl 
 |-  ( ( ( R e. _V /\ S e. _V ) /\ ( r = R /\ s = S ) ) -> ( s RingHom r ) = ( S RingHom R ) )
15 14 eleq2d 
 |-  ( ( ( R e. _V /\ S e. _V ) /\ ( r = R /\ s = S ) ) -> ( `' f e. ( s RingHom r ) <-> `' f e. ( S RingHom R ) ) )
16 11 15 rabeqbidv 
 |-  ( ( ( R e. _V /\ S e. _V ) /\ ( r = R /\ s = S ) ) -> { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } = { f e. ( R RingHom S ) | `' f e. ( S RingHom R ) } )
17 simpl 
 |-  ( ( R e. _V /\ S e. _V ) -> R e. _V )
18 simpr 
 |-  ( ( R e. _V /\ S e. _V ) -> S e. _V )
19 ovex 
 |-  ( R RingHom S ) e. _V
20 19 rabex 
 |-  { f e. ( R RingHom S ) | `' f e. ( S RingHom R ) } e. _V
21 20 a1i 
 |-  ( ( R e. _V /\ S e. _V ) -> { f e. ( R RingHom S ) | `' f e. ( S RingHom R ) } e. _V )
22 9 16 17 18 21 ovmpod 
 |-  ( ( R e. _V /\ S e. _V ) -> ( R RingIso S ) = { f e. ( R RingHom S ) | `' f e. ( S RingHom R ) } )
23 22 eleq2d 
 |-  ( ( R e. _V /\ S e. _V ) -> ( F e. ( R RingIso S ) <-> F e. { f e. ( R RingHom S ) | `' f e. ( S RingHom R ) } ) )
24 cnveq 
 |-  ( f = F -> `' f = `' F )
25 24 eleq1d 
 |-  ( f = F -> ( `' f e. ( S RingHom R ) <-> `' F e. ( S RingHom R ) ) )
26 25 elrab 
 |-  ( F e. { f e. ( R RingHom S ) | `' f e. ( S RingHom R ) } <-> ( F e. ( R RingHom S ) /\ `' F e. ( S RingHom R ) ) )
27 23 26 bitrdi 
 |-  ( ( R e. _V /\ S e. _V ) -> ( F e. ( R RingIso S ) <-> ( F e. ( R RingHom S ) /\ `' F e. ( S RingHom R ) ) ) )
28 1 7 27 pm5.21nii 
 |-  ( F e. ( R RingIso S ) <-> ( F e. ( R RingHom S ) /\ `' F e. ( S RingHom R ) ) )