Step | Hyp | Ref
| Expression |
1 | | df-sdrg 36785 |
. . . . 5
⊢ SubDRing
= (𝑤 ∈ DivRing ↦
{𝑠 ∈
(SubRing‘𝑤) ∣
(𝑤 ↾s
𝑠) ∈
DivRing}) |
2 | 1 | dmmptss 5548 |
. . . 4
⊢ dom
SubDRing ⊆ DivRing |
3 | | elfvdm 6130 |
. . . 4
⊢ (𝑆 ∈ (SubDRing‘𝑅) → 𝑅 ∈ dom SubDRing) |
4 | 2, 3 | sseldi 3566 |
. . 3
⊢ (𝑆 ∈ (SubDRing‘𝑅) → 𝑅 ∈ DivRing) |
5 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑤 = 𝑅 → (SubRing‘𝑤) = (SubRing‘𝑅)) |
6 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑤 = 𝑅 → (𝑤 ↾s 𝑠) = (𝑅 ↾s 𝑠)) |
7 | 6 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑤 = 𝑅 → ((𝑤 ↾s 𝑠) ∈ DivRing ↔ (𝑅 ↾s 𝑠) ∈ DivRing)) |
8 | 5, 7 | rabeqbidv 3168 |
. . . . . 6
⊢ (𝑤 = 𝑅 → {𝑠 ∈ (SubRing‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ DivRing} = {𝑠 ∈ (SubRing‘𝑅) ∣ (𝑅 ↾s 𝑠) ∈ DivRing}) |
9 | | fvex 6113 |
. . . . . . 7
⊢
(SubRing‘𝑅)
∈ V |
10 | 9 | rabex 4740 |
. . . . . 6
⊢ {𝑠 ∈ (SubRing‘𝑅) ∣ (𝑅 ↾s 𝑠) ∈ DivRing} ∈ V |
11 | 8, 1, 10 | fvmpt 6191 |
. . . . 5
⊢ (𝑅 ∈ DivRing →
(SubDRing‘𝑅) = {𝑠 ∈ (SubRing‘𝑅) ∣ (𝑅 ↾s 𝑠) ∈ DivRing}) |
12 | 11 | eleq2d 2673 |
. . . 4
⊢ (𝑅 ∈ DivRing → (𝑆 ∈ (SubDRing‘𝑅) ↔ 𝑆 ∈ {𝑠 ∈ (SubRing‘𝑅) ∣ (𝑅 ↾s 𝑠) ∈ DivRing})) |
13 | | oveq2 6557 |
. . . . . 6
⊢ (𝑠 = 𝑆 → (𝑅 ↾s 𝑠) = (𝑅 ↾s 𝑆)) |
14 | 13 | eleq1d 2672 |
. . . . 5
⊢ (𝑠 = 𝑆 → ((𝑅 ↾s 𝑠) ∈ DivRing ↔ (𝑅 ↾s 𝑆) ∈ DivRing)) |
15 | 14 | elrab 3331 |
. . . 4
⊢ (𝑆 ∈ {𝑠 ∈ (SubRing‘𝑅) ∣ (𝑅 ↾s 𝑠) ∈ DivRing} ↔ (𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing)) |
16 | 12, 15 | syl6bb 275 |
. . 3
⊢ (𝑅 ∈ DivRing → (𝑆 ∈ (SubDRing‘𝑅) ↔ (𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing))) |
17 | 4, 16 | biadan2 672 |
. 2
⊢ (𝑆 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ (𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing))) |
18 | | 3anass 1035 |
. 2
⊢ ((𝑅 ∈ DivRing ∧ 𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing) ↔ (𝑅 ∈ DivRing ∧ (𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing))) |
19 | 17, 18 | bitr4i 266 |
1
⊢ (𝑆 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ 𝑆 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑆) ∈ DivRing)) |