Step | Hyp | Ref
| Expression |
1 | | df-rngiso 19958 |
. . . . 5
⊢ RingIso
= (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RingHom 𝑠) ∣ ◡𝑓 ∈ (𝑠 RingHom 𝑟)}) |
2 | 1 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → RingIso = (𝑟 ∈ V, 𝑠 ∈ V ↦ {𝑓 ∈ (𝑟 RingHom 𝑠) ∣ ◡𝑓 ∈ (𝑠 RingHom 𝑟)})) |
3 | | oveq12 7286 |
. . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑟 RingHom 𝑠) = (𝑅 RingHom 𝑆)) |
4 | 3 | adantl 482 |
. . . . 5
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) ∧ (𝑟 = 𝑅 ∧ 𝑠 = 𝑆)) → (𝑟 RingHom 𝑠) = (𝑅 RingHom 𝑆)) |
5 | | oveq12 7286 |
. . . . . . . 8
⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (𝑠 RingHom 𝑟) = (𝑆 RingHom 𝑅)) |
6 | 5 | ancoms 459 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑠 RingHom 𝑟) = (𝑆 RingHom 𝑅)) |
7 | 6 | adantl 482 |
. . . . . 6
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) ∧ (𝑟 = 𝑅 ∧ 𝑠 = 𝑆)) → (𝑠 RingHom 𝑟) = (𝑆 RingHom 𝑅)) |
8 | 7 | eleq2d 2824 |
. . . . 5
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) ∧ (𝑟 = 𝑅 ∧ 𝑠 = 𝑆)) → (◡𝑓 ∈ (𝑠 RingHom 𝑟) ↔ ◡𝑓 ∈ (𝑆 RingHom 𝑅))) |
9 | 4, 8 | rabeqbidv 3419 |
. . . 4
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) ∧ (𝑟 = 𝑅 ∧ 𝑠 = 𝑆)) → {𝑓 ∈ (𝑟 RingHom 𝑠) ∣ ◡𝑓 ∈ (𝑠 RingHom 𝑟)} = {𝑓 ∈ (𝑅 RingHom 𝑆) ∣ ◡𝑓 ∈ (𝑆 RingHom 𝑅)}) |
10 | | elex 3449 |
. . . . 5
⊢ (𝑅 ∈ 𝑉 → 𝑅 ∈ V) |
11 | 10 | adantr 481 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → 𝑅 ∈ V) |
12 | | elex 3449 |
. . . . 5
⊢ (𝑆 ∈ 𝑊 → 𝑆 ∈ V) |
13 | 12 | adantl 482 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → 𝑆 ∈ V) |
14 | | ovex 7310 |
. . . . . 6
⊢ (𝑅 RingHom 𝑆) ∈ V |
15 | 14 | rabex 5258 |
. . . . 5
⊢ {𝑓 ∈ (𝑅 RingHom 𝑆) ∣ ◡𝑓 ∈ (𝑆 RingHom 𝑅)} ∈ V |
16 | 15 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → {𝑓 ∈ (𝑅 RingHom 𝑆) ∣ ◡𝑓 ∈ (𝑆 RingHom 𝑅)} ∈ V) |
17 | 2, 9, 11, 13, 16 | ovmpod 7425 |
. . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝑅 RingIso 𝑆) = {𝑓 ∈ (𝑅 RingHom 𝑆) ∣ ◡𝑓 ∈ (𝑆 RingHom 𝑅)}) |
18 | 17 | eleq2d 2824 |
. 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝐹 ∈ (𝑅 RingIso 𝑆) ↔ 𝐹 ∈ {𝑓 ∈ (𝑅 RingHom 𝑆) ∣ ◡𝑓 ∈ (𝑆 RingHom 𝑅)})) |
19 | | cnveq 5784 |
. . . 4
⊢ (𝑓 = 𝐹 → ◡𝑓 = ◡𝐹) |
20 | 19 | eleq1d 2823 |
. . 3
⊢ (𝑓 = 𝐹 → (◡𝑓 ∈ (𝑆 RingHom 𝑅) ↔ ◡𝐹 ∈ (𝑆 RingHom 𝑅))) |
21 | 20 | elrab 3625 |
. 2
⊢ (𝐹 ∈ {𝑓 ∈ (𝑅 RingHom 𝑆) ∣ ◡𝑓 ∈ (𝑆 RingHom 𝑅)} ↔ (𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ◡𝐹 ∈ (𝑆 RingHom 𝑅))) |
22 | 18, 21 | bitrdi 287 |
1
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝐹 ∈ (𝑅 RingIso 𝑆) ↔ (𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ◡𝐹 ∈ (𝑆 RingHom 𝑅)))) |