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-rngiso |
|- 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 ) ) ) |