Step | Hyp | Ref
| Expression |
1 | | df-subrg 19536 |
. . 3
⊢ SubRing =
(𝑟 ∈ Ring ↦
{𝑠 ∈ 𝒫
(Base‘𝑟) ∣
((𝑟 ↾s
𝑠) ∈ Ring ∧
(1r‘𝑟)
∈ 𝑠)}) |
2 | 1 | mptrcl 6780 |
. 2
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring) |
3 | | simpll 765 |
. 2
⊢ (((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴)) → 𝑅 ∈ Ring) |
4 | | fveq2 6673 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
5 | | issubrg.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑅) |
6 | 4, 5 | syl6eqr 2877 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵) |
7 | 6 | pweqd 4561 |
. . . . . 6
⊢ (𝑟 = 𝑅 → 𝒫 (Base‘𝑟) = 𝒫 𝐵) |
8 | | oveq1 7166 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (𝑟 ↾s 𝑠) = (𝑅 ↾s 𝑠)) |
9 | 8 | eleq1d 2900 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → ((𝑟 ↾s 𝑠) ∈ Ring ↔ (𝑅 ↾s 𝑠) ∈ Ring)) |
10 | | fveq2 6673 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (1r‘𝑟) = (1r‘𝑅)) |
11 | | issubrg.i |
. . . . . . . . 9
⊢ 1 =
(1r‘𝑅) |
12 | 10, 11 | syl6eqr 2877 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (1r‘𝑟) = 1 ) |
13 | 12 | eleq1d 2900 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → ((1r‘𝑟) ∈ 𝑠 ↔ 1 ∈ 𝑠)) |
14 | 9, 13 | anbi12d 632 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (((𝑟 ↾s 𝑠) ∈ Ring ∧
(1r‘𝑟)
∈ 𝑠) ↔ ((𝑅 ↾s 𝑠) ∈ Ring ∧ 1 ∈ 𝑠))) |
15 | 7, 14 | rabeqbidv 3488 |
. . . . 5
⊢ (𝑟 = 𝑅 → {𝑠 ∈ 𝒫 (Base‘𝑟) ∣ ((𝑟 ↾s 𝑠) ∈ Ring ∧
(1r‘𝑟)
∈ 𝑠)} = {𝑠 ∈ 𝒫 𝐵 ∣ ((𝑅 ↾s 𝑠) ∈ Ring ∧ 1 ∈ 𝑠)}) |
16 | 5 | fvexi 6687 |
. . . . . . 7
⊢ 𝐵 ∈ V |
17 | 16 | pwex 5284 |
. . . . . 6
⊢ 𝒫
𝐵 ∈ V |
18 | 17 | rabex 5238 |
. . . . 5
⊢ {𝑠 ∈ 𝒫 𝐵 ∣ ((𝑅 ↾s 𝑠) ∈ Ring ∧ 1 ∈ 𝑠)} ∈ V |
19 | 15, 1, 18 | fvmpt 6771 |
. . . 4
⊢ (𝑅 ∈ Ring →
(SubRing‘𝑅) = {𝑠 ∈ 𝒫 𝐵 ∣ ((𝑅 ↾s 𝑠) ∈ Ring ∧ 1 ∈ 𝑠)}) |
20 | 19 | eleq2d 2901 |
. . 3
⊢ (𝑅 ∈ Ring → (𝐴 ∈ (SubRing‘𝑅) ↔ 𝐴 ∈ {𝑠 ∈ 𝒫 𝐵 ∣ ((𝑅 ↾s 𝑠) ∈ Ring ∧ 1 ∈ 𝑠)})) |
21 | | oveq2 7167 |
. . . . . . . 8
⊢ (𝑠 = 𝐴 → (𝑅 ↾s 𝑠) = (𝑅 ↾s 𝐴)) |
22 | 21 | eleq1d 2900 |
. . . . . . 7
⊢ (𝑠 = 𝐴 → ((𝑅 ↾s 𝑠) ∈ Ring ↔ (𝑅 ↾s 𝐴) ∈ Ring)) |
23 | | eleq2 2904 |
. . . . . . 7
⊢ (𝑠 = 𝐴 → ( 1 ∈ 𝑠 ↔ 1 ∈ 𝐴)) |
24 | 22, 23 | anbi12d 632 |
. . . . . 6
⊢ (𝑠 = 𝐴 → (((𝑅 ↾s 𝑠) ∈ Ring ∧ 1 ∈ 𝑠) ↔ ((𝑅 ↾s 𝐴) ∈ Ring ∧ 1 ∈ 𝐴))) |
25 | 24 | elrab 3683 |
. . . . 5
⊢ (𝐴 ∈ {𝑠 ∈ 𝒫 𝐵 ∣ ((𝑅 ↾s 𝑠) ∈ Ring ∧ 1 ∈ 𝑠)} ↔ (𝐴 ∈ 𝒫 𝐵 ∧ ((𝑅 ↾s 𝐴) ∈ Ring ∧ 1 ∈ 𝐴))) |
26 | 16 | elpw2 5251 |
. . . . . 6
⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) |
27 | 26 | anbi1i 625 |
. . . . 5
⊢ ((𝐴 ∈ 𝒫 𝐵 ∧ ((𝑅 ↾s 𝐴) ∈ Ring ∧ 1 ∈ 𝐴)) ↔ (𝐴 ⊆ 𝐵 ∧ ((𝑅 ↾s 𝐴) ∈ Ring ∧ 1 ∈ 𝐴))) |
28 | | an12 643 |
. . . . 5
⊢ ((𝐴 ⊆ 𝐵 ∧ ((𝑅 ↾s 𝐴) ∈ Ring ∧ 1 ∈ 𝐴)) ↔ ((𝑅 ↾s 𝐴) ∈ Ring ∧ (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴))) |
29 | 25, 27, 28 | 3bitri 299 |
. . . 4
⊢ (𝐴 ∈ {𝑠 ∈ 𝒫 𝐵 ∣ ((𝑅 ↾s 𝑠) ∈ Ring ∧ 1 ∈ 𝑠)} ↔ ((𝑅 ↾s 𝐴) ∈ Ring ∧ (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴))) |
30 | | ibar 531 |
. . . . 5
⊢ (𝑅 ∈ Ring → ((𝑅 ↾s 𝐴) ∈ Ring ↔ (𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈
Ring))) |
31 | 30 | anbi1d 631 |
. . . 4
⊢ (𝑅 ∈ Ring → (((𝑅 ↾s 𝐴) ∈ Ring ∧ (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴)) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴)))) |
32 | 29, 31 | syl5bb 285 |
. . 3
⊢ (𝑅 ∈ Ring → (𝐴 ∈ {𝑠 ∈ 𝒫 𝐵 ∣ ((𝑅 ↾s 𝑠) ∈ Ring ∧ 1 ∈ 𝑠)} ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴)))) |
33 | 20, 32 | bitrd 281 |
. 2
⊢ (𝑅 ∈ Ring → (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴)))) |
34 | 2, 3, 33 | pm5.21nii 382 |
1
⊢ (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴))) |