Step |
Hyp |
Ref |
Expression |
1 |
|
rimrcl |
⊢ ( 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) → ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ) |
2 |
|
rhmrcl1 |
⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ Ring ) |
3 |
2
|
elexd |
⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ V ) |
4 |
|
rhmrcl2 |
⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑆 ∈ Ring ) |
5 |
4
|
elexd |
⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑆 ∈ V ) |
6 |
3 5
|
jca |
⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ) |
7 |
6
|
adantr |
⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 RingHom 𝑅 ) ) → ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ) |
8 |
|
df-rngiso |
⊢ RingIso = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ { 𝑓 ∈ ( 𝑟 RingHom 𝑠 ) ∣ ◡ 𝑓 ∈ ( 𝑠 RingHom 𝑟 ) } ) |
9 |
8
|
a1i |
⊢ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) → RingIso = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ { 𝑓 ∈ ( 𝑟 RingHom 𝑠 ) ∣ ◡ 𝑓 ∈ ( 𝑠 RingHom 𝑟 ) } ) ) |
10 |
|
oveq12 |
⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 𝑟 RingHom 𝑠 ) = ( 𝑅 RingHom 𝑆 ) ) |
11 |
10
|
adantl |
⊢ ( ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ∧ ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ) → ( 𝑟 RingHom 𝑠 ) = ( 𝑅 RingHom 𝑆 ) ) |
12 |
|
oveq12 |
⊢ ( ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) → ( 𝑠 RingHom 𝑟 ) = ( 𝑆 RingHom 𝑅 ) ) |
13 |
12
|
ancoms |
⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 𝑠 RingHom 𝑟 ) = ( 𝑆 RingHom 𝑅 ) ) |
14 |
13
|
adantl |
⊢ ( ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ∧ ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ) → ( 𝑠 RingHom 𝑟 ) = ( 𝑆 RingHom 𝑅 ) ) |
15 |
14
|
eleq2d |
⊢ ( ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ∧ ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ) → ( ◡ 𝑓 ∈ ( 𝑠 RingHom 𝑟 ) ↔ ◡ 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) ) ) |
16 |
11 15
|
rabeqbidv |
⊢ ( ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ∧ ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ) → { 𝑓 ∈ ( 𝑟 RingHom 𝑠 ) ∣ ◡ 𝑓 ∈ ( 𝑠 RingHom 𝑟 ) } = { 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) ∣ ◡ 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) } ) |
17 |
|
simpl |
⊢ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) → 𝑅 ∈ V ) |
18 |
|
simpr |
⊢ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) → 𝑆 ∈ V ) |
19 |
|
ovex |
⊢ ( 𝑅 RingHom 𝑆 ) ∈ V |
20 |
19
|
rabex |
⊢ { 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) ∣ ◡ 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) } ∈ V |
21 |
20
|
a1i |
⊢ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) → { 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) ∣ ◡ 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) } ∈ V ) |
22 |
9 16 17 18 21
|
ovmpod |
⊢ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) → ( 𝑅 RingIso 𝑆 ) = { 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) ∣ ◡ 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) } ) |
23 |
22
|
eleq2d |
⊢ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) → ( 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) ↔ 𝐹 ∈ { 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) ∣ ◡ 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) } ) ) |
24 |
|
cnveq |
⊢ ( 𝑓 = 𝐹 → ◡ 𝑓 = ◡ 𝐹 ) |
25 |
24
|
eleq1d |
⊢ ( 𝑓 = 𝐹 → ( ◡ 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) ↔ ◡ 𝐹 ∈ ( 𝑆 RingHom 𝑅 ) ) ) |
26 |
25
|
elrab |
⊢ ( 𝐹 ∈ { 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) ∣ ◡ 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) } ↔ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 RingHom 𝑅 ) ) ) |
27 |
23 26
|
bitrdi |
⊢ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) → ( 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 RingHom 𝑅 ) ) ) ) |
28 |
1 7 27
|
pm5.21nii |
⊢ ( 𝐹 ∈ ( 𝑅 RingIso 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 RingHom 𝑅 ) ) ) |