Step | Hyp | Ref
| Expression |
1 | | df-subrg 18778 |
. . 3
⊢ SubRing =
(𝑟 ∈ Ring ↦
{𝑠 ∈ 𝒫
(Base‘𝑟) ∣
((𝑟 ↾s
𝑠) ∈ Ring ∧
(1r‘𝑟)
∈ 𝑠)}) |
2 | 1 | mptrcl 6289 |
. 2
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring) |
3 | | simpll 790 |
. 2
⊢ (((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴)) → 𝑅 ∈ Ring) |
4 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
5 | | issubrg.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑅) |
6 | 4, 5 | syl6eqr 2674 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵) |
7 | 6 | pweqd 4163 |
. . . . . 6
⊢ (𝑟 = 𝑅 → 𝒫 (Base‘𝑟) = 𝒫 𝐵) |
8 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (𝑟 ↾s 𝑠) = (𝑅 ↾s 𝑠)) |
9 | 8 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → ((𝑟 ↾s 𝑠) ∈ Ring ↔ (𝑅 ↾s 𝑠) ∈ Ring)) |
10 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (1r‘𝑟) = (1r‘𝑅)) |
11 | | issubrg.i |
. . . . . . . . 9
⊢ 1 =
(1r‘𝑅) |
12 | 10, 11 | syl6eqr 2674 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (1r‘𝑟) = 1 ) |
13 | 12 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → ((1r‘𝑟) ∈ 𝑠 ↔ 1 ∈ 𝑠)) |
14 | 9, 13 | anbi12d 747 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (((𝑟 ↾s 𝑠) ∈ Ring ∧
(1r‘𝑟)
∈ 𝑠) ↔ ((𝑅 ↾s 𝑠) ∈ Ring ∧ 1 ∈ 𝑠))) |
15 | 7, 14 | rabeqbidv 3195 |
. . . . 5
⊢ (𝑟 = 𝑅 → {𝑠 ∈ 𝒫 (Base‘𝑟) ∣ ((𝑟 ↾s 𝑠) ∈ Ring ∧
(1r‘𝑟)
∈ 𝑠)} = {𝑠 ∈ 𝒫 𝐵 ∣ ((𝑅 ↾s 𝑠) ∈ Ring ∧ 1 ∈ 𝑠)}) |
16 | | fvex 6201 |
. . . . . . . 8
⊢
(Base‘𝑅)
∈ V |
17 | 5, 16 | eqeltri 2697 |
. . . . . . 7
⊢ 𝐵 ∈ V |
18 | 17 | pwex 4848 |
. . . . . 6
⊢ 𝒫
𝐵 ∈ V |
19 | 18 | rabex 4813 |
. . . . 5
⊢ {𝑠 ∈ 𝒫 𝐵 ∣ ((𝑅 ↾s 𝑠) ∈ Ring ∧ 1 ∈ 𝑠)} ∈ V |
20 | 15, 1, 19 | fvmpt 6282 |
. . . 4
⊢ (𝑅 ∈ Ring →
(SubRing‘𝑅) = {𝑠 ∈ 𝒫 𝐵 ∣ ((𝑅 ↾s 𝑠) ∈ Ring ∧ 1 ∈ 𝑠)}) |
21 | 20 | eleq2d 2687 |
. . 3
⊢ (𝑅 ∈ Ring → (𝐴 ∈ (SubRing‘𝑅) ↔ 𝐴 ∈ {𝑠 ∈ 𝒫 𝐵 ∣ ((𝑅 ↾s 𝑠) ∈ Ring ∧ 1 ∈ 𝑠)})) |
22 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑠 = 𝐴 → (𝑅 ↾s 𝑠) = (𝑅 ↾s 𝐴)) |
23 | 22 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑠 = 𝐴 → ((𝑅 ↾s 𝑠) ∈ Ring ↔ (𝑅 ↾s 𝐴) ∈ Ring)) |
24 | | eleq2 2690 |
. . . . . . 7
⊢ (𝑠 = 𝐴 → ( 1 ∈ 𝑠 ↔ 1 ∈ 𝐴)) |
25 | 23, 24 | anbi12d 747 |
. . . . . 6
⊢ (𝑠 = 𝐴 → (((𝑅 ↾s 𝑠) ∈ Ring ∧ 1 ∈ 𝑠) ↔ ((𝑅 ↾s 𝐴) ∈ Ring ∧ 1 ∈ 𝐴))) |
26 | 25 | elrab 3363 |
. . . . 5
⊢ (𝐴 ∈ {𝑠 ∈ 𝒫 𝐵 ∣ ((𝑅 ↾s 𝑠) ∈ Ring ∧ 1 ∈ 𝑠)} ↔ (𝐴 ∈ 𝒫 𝐵 ∧ ((𝑅 ↾s 𝐴) ∈ Ring ∧ 1 ∈ 𝐴))) |
27 | 17 | elpw2 4828 |
. . . . . 6
⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) |
28 | 27 | anbi1i 731 |
. . . . 5
⊢ ((𝐴 ∈ 𝒫 𝐵 ∧ ((𝑅 ↾s 𝐴) ∈ Ring ∧ 1 ∈ 𝐴)) ↔ (𝐴 ⊆ 𝐵 ∧ ((𝑅 ↾s 𝐴) ∈ Ring ∧ 1 ∈ 𝐴))) |
29 | | an12 838 |
. . . . 5
⊢ ((𝐴 ⊆ 𝐵 ∧ ((𝑅 ↾s 𝐴) ∈ Ring ∧ 1 ∈ 𝐴)) ↔ ((𝑅 ↾s 𝐴) ∈ Ring ∧ (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴))) |
30 | 26, 28, 29 | 3bitri 286 |
. . . 4
⊢ (𝐴 ∈ {𝑠 ∈ 𝒫 𝐵 ∣ ((𝑅 ↾s 𝑠) ∈ Ring ∧ 1 ∈ 𝑠)} ↔ ((𝑅 ↾s 𝐴) ∈ Ring ∧ (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴))) |
31 | | ibar 525 |
. . . . 5
⊢ (𝑅 ∈ Ring → ((𝑅 ↾s 𝐴) ∈ Ring ↔ (𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈
Ring))) |
32 | 31 | anbi1d 741 |
. . . 4
⊢ (𝑅 ∈ Ring → (((𝑅 ↾s 𝐴) ∈ Ring ∧ (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴)) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴)))) |
33 | 30, 32 | syl5bb 272 |
. . 3
⊢ (𝑅 ∈ Ring → (𝐴 ∈ {𝑠 ∈ 𝒫 𝐵 ∣ ((𝑅 ↾s 𝑠) ∈ Ring ∧ 1 ∈ 𝑠)} ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴)))) |
34 | 21, 33 | bitrd 268 |
. 2
⊢ (𝑅 ∈ Ring → (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴)))) |
35 | 2, 3, 34 | pm5.21nii 368 |
1
⊢ (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴))) |