Step | Hyp | Ref
| Expression |
1 | | eqid 2821 |
. . . . . . . 8
⊢
(invr‘𝑅) = (invr‘𝑅) |
2 | | eqid 2821 |
. . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) |
3 | 1, 2 | issdrg2 19571 |
. . . . . . 7
⊢ (𝑠 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ 𝑠 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠)) |
4 | | 3anass 1091 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝑠 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠) ↔ (𝑅 ∈ DivRing ∧ (𝑠 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠))) |
5 | 3, 4 | bitri 277 |
. . . . . 6
⊢ (𝑠 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ (𝑠 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠))) |
6 | 5 | baib 538 |
. . . . 5
⊢ (𝑅 ∈ DivRing → (𝑠 ∈ (SubDRing‘𝑅) ↔ (𝑠 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠))) |
7 | | subrgacs.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑅) |
8 | 7 | subrgss 19530 |
. . . . . . . . 9
⊢ (𝑠 ∈ (SubRing‘𝑅) → 𝑠 ⊆ 𝐵) |
9 | | velpw 4546 |
. . . . . . . . 9
⊢ (𝑠 ∈ 𝒫 𝐵 ↔ 𝑠 ⊆ 𝐵) |
10 | 8, 9 | sylibr 236 |
. . . . . . . 8
⊢ (𝑠 ∈ (SubRing‘𝑅) → 𝑠 ∈ 𝒫 𝐵) |
11 | 10 | adantl 484 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝑠 ∈ (SubRing‘𝑅)) → 𝑠 ∈ 𝒫 𝐵) |
12 | | iftrue 4472 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (0g‘𝑅) → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) = 𝑥) |
13 | 12 | eleq1d 2897 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (0g‘𝑅) → (if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦 ↔ 𝑥 ∈ 𝑦)) |
14 | 13 | biimprd 250 |
. . . . . . . . . . . 12
⊢ (𝑥 = (0g‘𝑅) → (𝑥 ∈ 𝑦 → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦)) |
15 | | eldifsni 4715 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}) → 𝑥 ≠ (0g‘𝑅)) |
16 | 15 | necon2bi 3046 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (0g‘𝑅) → ¬ 𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)})) |
17 | 16 | pm2.21d 121 |
. . . . . . . . . . . 12
⊢ (𝑥 = (0g‘𝑅) → (𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}) →
((invr‘𝑅)‘𝑥) ∈ 𝑦)) |
18 | 14, 17 | 2thd 267 |
. . . . . . . . . . 11
⊢ (𝑥 = (0g‘𝑅) → ((𝑥 ∈ 𝑦 → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦) ↔ (𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}) →
((invr‘𝑅)‘𝑥) ∈ 𝑦))) |
19 | | eldifsn 4712 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}) ↔ (𝑥 ∈ 𝑦 ∧ 𝑥 ≠ (0g‘𝑅))) |
20 | 19 | rbaibr 540 |
. . . . . . . . . . . 12
⊢ (𝑥 ≠ (0g‘𝑅) → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}))) |
21 | | ifnefalse 4478 |
. . . . . . . . . . . . 13
⊢ (𝑥 ≠ (0g‘𝑅) → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) = ((invr‘𝑅)‘𝑥)) |
22 | 21 | eleq1d 2897 |
. . . . . . . . . . . 12
⊢ (𝑥 ≠ (0g‘𝑅) → (if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦 ↔ ((invr‘𝑅)‘𝑥) ∈ 𝑦)) |
23 | 20, 22 | imbi12d 347 |
. . . . . . . . . . 11
⊢ (𝑥 ≠ (0g‘𝑅) → ((𝑥 ∈ 𝑦 → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦) ↔ (𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}) →
((invr‘𝑅)‘𝑥) ∈ 𝑦))) |
24 | 18, 23 | pm2.61ine 3100 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑦 → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦) ↔ (𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}) →
((invr‘𝑅)‘𝑥) ∈ 𝑦)) |
25 | 24 | ralbii2 3163 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦 ↔ ∀𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑦) |
26 | | difeq1 4091 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑠 → (𝑦 ∖ {(0g‘𝑅)}) = (𝑠 ∖ {(0g‘𝑅)})) |
27 | | eleq2w 2896 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑠 → (((invr‘𝑅)‘𝑥) ∈ 𝑦 ↔ ((invr‘𝑅)‘𝑥) ∈ 𝑠)) |
28 | 26, 27 | raleqbidv 3401 |
. . . . . . . . 9
⊢ (𝑦 = 𝑠 → (∀𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑦 ↔ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠)) |
29 | 25, 28 | syl5bb 285 |
. . . . . . . 8
⊢ (𝑦 = 𝑠 → (∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦 ↔ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠)) |
30 | 29 | elrab3 3680 |
. . . . . . 7
⊢ (𝑠 ∈ 𝒫 𝐵 → (𝑠 ∈ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦} ↔ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠)) |
31 | 11, 30 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ 𝑠 ∈ (SubRing‘𝑅)) → (𝑠 ∈ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦} ↔ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠)) |
32 | 31 | pm5.32da 581 |
. . . . 5
⊢ (𝑅 ∈ DivRing → ((𝑠 ∈ (SubRing‘𝑅) ∧ 𝑠 ∈ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦}) ↔ (𝑠 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠))) |
33 | 6, 32 | bitr4d 284 |
. . . 4
⊢ (𝑅 ∈ DivRing → (𝑠 ∈ (SubDRing‘𝑅) ↔ (𝑠 ∈ (SubRing‘𝑅) ∧ 𝑠 ∈ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦}))) |
34 | | elin 4168 |
. . . 4
⊢ (𝑠 ∈ ((SubRing‘𝑅) ∩ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦}) ↔ (𝑠 ∈ (SubRing‘𝑅) ∧ 𝑠 ∈ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦})) |
35 | 33, 34 | syl6bbr 291 |
. . 3
⊢ (𝑅 ∈ DivRing → (𝑠 ∈ (SubDRing‘𝑅) ↔ 𝑠 ∈ ((SubRing‘𝑅) ∩ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦}))) |
36 | 35 | eqrdv 2819 |
. 2
⊢ (𝑅 ∈ DivRing →
(SubDRing‘𝑅) =
((SubRing‘𝑅) ∩
{𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦})) |
37 | 7 | fvexi 6678 |
. . . 4
⊢ 𝐵 ∈ V |
38 | | mreacs 16923 |
. . . 4
⊢ (𝐵 ∈ V →
(ACS‘𝐵) ∈
(Moore‘𝒫 𝐵)) |
39 | 37, 38 | mp1i 13 |
. . 3
⊢ (𝑅 ∈ DivRing →
(ACS‘𝐵) ∈
(Moore‘𝒫 𝐵)) |
40 | | drngring 19503 |
. . . 4
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
41 | 7 | subrgacs 19573 |
. . . 4
⊢ (𝑅 ∈ Ring →
(SubRing‘𝑅) ∈
(ACS‘𝐵)) |
42 | 40, 41 | syl 17 |
. . 3
⊢ (𝑅 ∈ DivRing →
(SubRing‘𝑅) ∈
(ACS‘𝐵)) |
43 | | simplr 767 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 = (0g‘𝑅)) → 𝑥 ∈ 𝐵) |
44 | | df-ne 3017 |
. . . . . . 7
⊢ (𝑥 ≠ (0g‘𝑅) ↔ ¬ 𝑥 = (0g‘𝑅)) |
45 | 7, 2, 1 | drnginvrcl 19513 |
. . . . . . . 8
⊢ ((𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝑅)) → ((invr‘𝑅)‘𝑥) ∈ 𝐵) |
46 | 45 | 3expa 1114 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ≠ (0g‘𝑅)) → ((invr‘𝑅)‘𝑥) ∈ 𝐵) |
47 | 44, 46 | sylan2br 596 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵) ∧ ¬ 𝑥 = (0g‘𝑅)) → ((invr‘𝑅)‘𝑥) ∈ 𝐵) |
48 | 43, 47 | ifclda 4500 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵) → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝐵) |
49 | 48 | ralrimiva 3182 |
. . . 4
⊢ (𝑅 ∈ DivRing →
∀𝑥 ∈ 𝐵 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝐵) |
50 | | acsfn1 16926 |
. . . 4
⊢ ((𝐵 ∈ V ∧ ∀𝑥 ∈ 𝐵 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝐵) → {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦} ∈ (ACS‘𝐵)) |
51 | 37, 49, 50 | sylancr 589 |
. . 3
⊢ (𝑅 ∈ DivRing → {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦} ∈ (ACS‘𝐵)) |
52 | | mreincl 16864 |
. . 3
⊢
(((ACS‘𝐵)
∈ (Moore‘𝒫 𝐵) ∧ (SubRing‘𝑅) ∈ (ACS‘𝐵) ∧ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦} ∈ (ACS‘𝐵)) → ((SubRing‘𝑅) ∩ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦}) ∈ (ACS‘𝐵)) |
53 | 39, 42, 51, 52 | syl3anc 1367 |
. 2
⊢ (𝑅 ∈ DivRing →
((SubRing‘𝑅) ∩
{𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦}) ∈ (ACS‘𝐵)) |
54 | 36, 53 | eqeltrd 2913 |
1
⊢ (𝑅 ∈ DivRing →
(SubDRing‘𝑅) ∈
(ACS‘𝐵)) |