Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . . . . . 8
⊢
(invr‘𝑅) = (invr‘𝑅) |
2 | | eqid 2738 |
. . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) |
3 | 1, 2 | issdrg2 19981 |
. . . . . . 7
⊢ (𝑠 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ 𝑠 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠)) |
4 | | 3anass 1093 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝑠 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠) ↔ (𝑅 ∈ DivRing ∧ (𝑠 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠))) |
5 | 3, 4 | bitri 274 |
. . . . . 6
⊢ (𝑠 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ (𝑠 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠))) |
6 | 5 | baib 535 |
. . . . 5
⊢ (𝑅 ∈ DivRing → (𝑠 ∈ (SubDRing‘𝑅) ↔ (𝑠 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠))) |
7 | | subrgacs.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑅) |
8 | 7 | subrgss 19940 |
. . . . . . . . 9
⊢ (𝑠 ∈ (SubRing‘𝑅) → 𝑠 ⊆ 𝐵) |
9 | | velpw 4535 |
. . . . . . . . 9
⊢ (𝑠 ∈ 𝒫 𝐵 ↔ 𝑠 ⊆ 𝐵) |
10 | 8, 9 | sylibr 233 |
. . . . . . . 8
⊢ (𝑠 ∈ (SubRing‘𝑅) → 𝑠 ∈ 𝒫 𝐵) |
11 | 10 | adantl 481 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝑠 ∈ (SubRing‘𝑅)) → 𝑠 ∈ 𝒫 𝐵) |
12 | | iftrue 4462 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (0g‘𝑅) → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) = 𝑥) |
13 | 12 | eleq1d 2823 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (0g‘𝑅) → (if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦 ↔ 𝑥 ∈ 𝑦)) |
14 | 13 | biimprd 247 |
. . . . . . . . . . . 12
⊢ (𝑥 = (0g‘𝑅) → (𝑥 ∈ 𝑦 → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦)) |
15 | | eldifsni 4720 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}) → 𝑥 ≠ (0g‘𝑅)) |
16 | 15 | necon2bi 2973 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (0g‘𝑅) → ¬ 𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)})) |
17 | 16 | pm2.21d 121 |
. . . . . . . . . . . 12
⊢ (𝑥 = (0g‘𝑅) → (𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}) →
((invr‘𝑅)‘𝑥) ∈ 𝑦)) |
18 | 14, 17 | 2thd 264 |
. . . . . . . . . . 11
⊢ (𝑥 = (0g‘𝑅) → ((𝑥 ∈ 𝑦 → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦) ↔ (𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}) →
((invr‘𝑅)‘𝑥) ∈ 𝑦))) |
19 | | eldifsn 4717 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}) ↔ (𝑥 ∈ 𝑦 ∧ 𝑥 ≠ (0g‘𝑅))) |
20 | 19 | rbaibr 537 |
. . . . . . . . . . . 12
⊢ (𝑥 ≠ (0g‘𝑅) → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}))) |
21 | | ifnefalse 4468 |
. . . . . . . . . . . . 13
⊢ (𝑥 ≠ (0g‘𝑅) → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) = ((invr‘𝑅)‘𝑥)) |
22 | 21 | eleq1d 2823 |
. . . . . . . . . . . 12
⊢ (𝑥 ≠ (0g‘𝑅) → (if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦 ↔ ((invr‘𝑅)‘𝑥) ∈ 𝑦)) |
23 | 20, 22 | imbi12d 344 |
. . . . . . . . . . 11
⊢ (𝑥 ≠ (0g‘𝑅) → ((𝑥 ∈ 𝑦 → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦) ↔ (𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}) →
((invr‘𝑅)‘𝑥) ∈ 𝑦))) |
24 | 18, 23 | pm2.61ine 3027 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑦 → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦) ↔ (𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}) →
((invr‘𝑅)‘𝑥) ∈ 𝑦)) |
25 | 24 | ralbii2 3088 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦 ↔ ∀𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑦) |
26 | | difeq1 4046 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑠 → (𝑦 ∖ {(0g‘𝑅)}) = (𝑠 ∖ {(0g‘𝑅)})) |
27 | | eleq2w 2822 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑠 → (((invr‘𝑅)‘𝑥) ∈ 𝑦 ↔ ((invr‘𝑅)‘𝑥) ∈ 𝑠)) |
28 | 26, 27 | raleqbidv 3327 |
. . . . . . . . 9
⊢ (𝑦 = 𝑠 → (∀𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑦 ↔ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠)) |
29 | 25, 28 | syl5bb 282 |
. . . . . . . 8
⊢ (𝑦 = 𝑠 → (∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦 ↔ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠)) |
30 | 29 | elrab3 3618 |
. . . . . . 7
⊢ (𝑠 ∈ 𝒫 𝐵 → (𝑠 ∈ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦} ↔ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠)) |
31 | 11, 30 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ 𝑠 ∈ (SubRing‘𝑅)) → (𝑠 ∈ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦} ↔ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠)) |
32 | 31 | pm5.32da 578 |
. . . . 5
⊢ (𝑅 ∈ DivRing → ((𝑠 ∈ (SubRing‘𝑅) ∧ 𝑠 ∈ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦}) ↔ (𝑠 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠))) |
33 | 6, 32 | bitr4d 281 |
. . . 4
⊢ (𝑅 ∈ DivRing → (𝑠 ∈ (SubDRing‘𝑅) ↔ (𝑠 ∈ (SubRing‘𝑅) ∧ 𝑠 ∈ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦}))) |
34 | | elin 3899 |
. . . 4
⊢ (𝑠 ∈ ((SubRing‘𝑅) ∩ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦}) ↔ (𝑠 ∈ (SubRing‘𝑅) ∧ 𝑠 ∈ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦})) |
35 | 33, 34 | bitr4di 288 |
. . 3
⊢ (𝑅 ∈ DivRing → (𝑠 ∈ (SubDRing‘𝑅) ↔ 𝑠 ∈ ((SubRing‘𝑅) ∩ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦}))) |
36 | 35 | eqrdv 2736 |
. 2
⊢ (𝑅 ∈ DivRing →
(SubDRing‘𝑅) =
((SubRing‘𝑅) ∩
{𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦})) |
37 | 7 | fvexi 6770 |
. . . 4
⊢ 𝐵 ∈ V |
38 | | mreacs 17284 |
. . . 4
⊢ (𝐵 ∈ V →
(ACS‘𝐵) ∈
(Moore‘𝒫 𝐵)) |
39 | 37, 38 | mp1i 13 |
. . 3
⊢ (𝑅 ∈ DivRing →
(ACS‘𝐵) ∈
(Moore‘𝒫 𝐵)) |
40 | | drngring 19913 |
. . . 4
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
41 | 7 | subrgacs 19983 |
. . . 4
⊢ (𝑅 ∈ Ring →
(SubRing‘𝑅) ∈
(ACS‘𝐵)) |
42 | 40, 41 | syl 17 |
. . 3
⊢ (𝑅 ∈ DivRing →
(SubRing‘𝑅) ∈
(ACS‘𝐵)) |
43 | | simplr 765 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 = (0g‘𝑅)) → 𝑥 ∈ 𝐵) |
44 | | df-ne 2943 |
. . . . . . 7
⊢ (𝑥 ≠ (0g‘𝑅) ↔ ¬ 𝑥 = (0g‘𝑅)) |
45 | 7, 2, 1 | drnginvrcl 19923 |
. . . . . . . 8
⊢ ((𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝑅)) → ((invr‘𝑅)‘𝑥) ∈ 𝐵) |
46 | 45 | 3expa 1116 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ≠ (0g‘𝑅)) → ((invr‘𝑅)‘𝑥) ∈ 𝐵) |
47 | 44, 46 | sylan2br 594 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵) ∧ ¬ 𝑥 = (0g‘𝑅)) → ((invr‘𝑅)‘𝑥) ∈ 𝐵) |
48 | 43, 47 | ifclda 4491 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵) → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝐵) |
49 | 48 | ralrimiva 3107 |
. . . 4
⊢ (𝑅 ∈ DivRing →
∀𝑥 ∈ 𝐵 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝐵) |
50 | | acsfn1 17287 |
. . . 4
⊢ ((𝐵 ∈ V ∧ ∀𝑥 ∈ 𝐵 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝐵) → {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦} ∈ (ACS‘𝐵)) |
51 | 37, 49, 50 | sylancr 586 |
. . 3
⊢ (𝑅 ∈ DivRing → {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦} ∈ (ACS‘𝐵)) |
52 | | mreincl 17225 |
. . 3
⊢
(((ACS‘𝐵)
∈ (Moore‘𝒫 𝐵) ∧ (SubRing‘𝑅) ∈ (ACS‘𝐵) ∧ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦} ∈ (ACS‘𝐵)) → ((SubRing‘𝑅) ∩ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦}) ∈ (ACS‘𝐵)) |
53 | 39, 42, 51, 52 | syl3anc 1369 |
. 2
⊢ (𝑅 ∈ DivRing →
((SubRing‘𝑅) ∩
{𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦}) ∈ (ACS‘𝐵)) |
54 | 36, 53 | eqeltrd 2839 |
1
⊢ (𝑅 ∈ DivRing →
(SubDRing‘𝑅) ∈
(ACS‘𝐵)) |