Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . . . . 8
⊢
(invr‘𝑅) = (invr‘𝑅) |
2 | | eqid 2610 |
. . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) |
3 | 1, 2 | issdrg2 36787 |
. . . . . . 7
⊢ (𝑠 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ 𝑠 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠)) |
4 | | 3anass 1035 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝑠 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠) ↔ (𝑅 ∈ DivRing ∧ (𝑠 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠))) |
5 | 3, 4 | bitri 263 |
. . . . . 6
⊢ (𝑠 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ (𝑠 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠))) |
6 | 5 | baib 942 |
. . . . 5
⊢ (𝑅 ∈ DivRing → (𝑠 ∈ (SubDRing‘𝑅) ↔ (𝑠 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠))) |
7 | | subrgacs.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑅) |
8 | 7 | subrgss 18604 |
. . . . . . . . 9
⊢ (𝑠 ∈ (SubRing‘𝑅) → 𝑠 ⊆ 𝐵) |
9 | | selpw 4115 |
. . . . . . . . 9
⊢ (𝑠 ∈ 𝒫 𝐵 ↔ 𝑠 ⊆ 𝐵) |
10 | 8, 9 | sylibr 223 |
. . . . . . . 8
⊢ (𝑠 ∈ (SubRing‘𝑅) → 𝑠 ∈ 𝒫 𝐵) |
11 | 10 | adantl 481 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝑠 ∈ (SubRing‘𝑅)) → 𝑠 ∈ 𝒫 𝐵) |
12 | | iftrue 4042 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (0g‘𝑅) → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) = 𝑥) |
13 | 12 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (0g‘𝑅) → (if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦 ↔ 𝑥 ∈ 𝑦)) |
14 | 13 | biimprd 237 |
. . . . . . . . . . . 12
⊢ (𝑥 = (0g‘𝑅) → (𝑥 ∈ 𝑦 → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦)) |
15 | | eldifsni 4261 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}) → 𝑥 ≠ (0g‘𝑅)) |
16 | 15 | necon2bi 2812 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (0g‘𝑅) → ¬ 𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)})) |
17 | 16 | pm2.21d 117 |
. . . . . . . . . . . 12
⊢ (𝑥 = (0g‘𝑅) → (𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}) →
((invr‘𝑅)‘𝑥) ∈ 𝑦)) |
18 | 14, 17 | 2thd 254 |
. . . . . . . . . . 11
⊢ (𝑥 = (0g‘𝑅) → ((𝑥 ∈ 𝑦 → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦) ↔ (𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}) →
((invr‘𝑅)‘𝑥) ∈ 𝑦))) |
19 | | eldifsn 4260 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}) ↔ (𝑥 ∈ 𝑦 ∧ 𝑥 ≠ (0g‘𝑅))) |
20 | 19 | rbaibr 944 |
. . . . . . . . . . . 12
⊢ (𝑥 ≠ (0g‘𝑅) → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}))) |
21 | | ifnefalse 4048 |
. . . . . . . . . . . . 13
⊢ (𝑥 ≠ (0g‘𝑅) → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) = ((invr‘𝑅)‘𝑥)) |
22 | 21 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝑥 ≠ (0g‘𝑅) → (if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦 ↔ ((invr‘𝑅)‘𝑥) ∈ 𝑦)) |
23 | 20, 22 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑥 ≠ (0g‘𝑅) → ((𝑥 ∈ 𝑦 → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦) ↔ (𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}) →
((invr‘𝑅)‘𝑥) ∈ 𝑦))) |
24 | 18, 23 | pm2.61ine 2865 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑦 → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦) ↔ (𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}) →
((invr‘𝑅)‘𝑥) ∈ 𝑦)) |
25 | 24 | ralbii2 2961 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦 ↔ ∀𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑦) |
26 | | difeq1 3683 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑠 → (𝑦 ∖ {(0g‘𝑅)}) = (𝑠 ∖ {(0g‘𝑅)})) |
27 | | eleq2 2677 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑠 → (((invr‘𝑅)‘𝑥) ∈ 𝑦 ↔ ((invr‘𝑅)‘𝑥) ∈ 𝑠)) |
28 | 26, 27 | raleqbidv 3129 |
. . . . . . . . 9
⊢ (𝑦 = 𝑠 → (∀𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑦 ↔ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠)) |
29 | 25, 28 | syl5bb 271 |
. . . . . . . 8
⊢ (𝑦 = 𝑠 → (∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦 ↔ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠)) |
30 | 29 | elrab3 3332 |
. . . . . . 7
⊢ (𝑠 ∈ 𝒫 𝐵 → (𝑠 ∈ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦} ↔ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠)) |
31 | 11, 30 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ 𝑠 ∈ (SubRing‘𝑅)) → (𝑠 ∈ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦} ↔ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠)) |
32 | 31 | pm5.32da 671 |
. . . . 5
⊢ (𝑅 ∈ DivRing → ((𝑠 ∈ (SubRing‘𝑅) ∧ 𝑠 ∈ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦}) ↔ (𝑠 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠))) |
33 | 6, 32 | bitr4d 270 |
. . . 4
⊢ (𝑅 ∈ DivRing → (𝑠 ∈ (SubDRing‘𝑅) ↔ (𝑠 ∈ (SubRing‘𝑅) ∧ 𝑠 ∈ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦}))) |
34 | | elin 3758 |
. . . 4
⊢ (𝑠 ∈ ((SubRing‘𝑅) ∩ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦}) ↔ (𝑠 ∈ (SubRing‘𝑅) ∧ 𝑠 ∈ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦})) |
35 | 33, 34 | syl6bbr 277 |
. . 3
⊢ (𝑅 ∈ DivRing → (𝑠 ∈ (SubDRing‘𝑅) ↔ 𝑠 ∈ ((SubRing‘𝑅) ∩ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦}))) |
36 | 35 | eqrdv 2608 |
. 2
⊢ (𝑅 ∈ DivRing →
(SubDRing‘𝑅) =
((SubRing‘𝑅) ∩
{𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦})) |
37 | | fvex 6113 |
. . . . 5
⊢
(Base‘𝑅)
∈ V |
38 | 7, 37 | eqeltri 2684 |
. . . 4
⊢ 𝐵 ∈ V |
39 | | mreacs 16142 |
. . . 4
⊢ (𝐵 ∈ V →
(ACS‘𝐵) ∈
(Moore‘𝒫 𝐵)) |
40 | 38, 39 | mp1i 13 |
. . 3
⊢ (𝑅 ∈ DivRing →
(ACS‘𝐵) ∈
(Moore‘𝒫 𝐵)) |
41 | | drngring 18577 |
. . . 4
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
42 | 7 | subrgacs 36789 |
. . . 4
⊢ (𝑅 ∈ Ring →
(SubRing‘𝑅) ∈
(ACS‘𝐵)) |
43 | 41, 42 | syl 17 |
. . 3
⊢ (𝑅 ∈ DivRing →
(SubRing‘𝑅) ∈
(ACS‘𝐵)) |
44 | | simplr 788 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 = (0g‘𝑅)) → 𝑥 ∈ 𝐵) |
45 | | df-ne 2782 |
. . . . . . 7
⊢ (𝑥 ≠ (0g‘𝑅) ↔ ¬ 𝑥 = (0g‘𝑅)) |
46 | 7, 2, 1 | drnginvrcl 18587 |
. . . . . . . 8
⊢ ((𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝑅)) → ((invr‘𝑅)‘𝑥) ∈ 𝐵) |
47 | 46 | 3expa 1257 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ≠ (0g‘𝑅)) → ((invr‘𝑅)‘𝑥) ∈ 𝐵) |
48 | 45, 47 | sylan2br 492 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵) ∧ ¬ 𝑥 = (0g‘𝑅)) → ((invr‘𝑅)‘𝑥) ∈ 𝐵) |
49 | 44, 48 | ifclda 4070 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵) → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝐵) |
50 | 49 | ralrimiva 2949 |
. . . 4
⊢ (𝑅 ∈ DivRing →
∀𝑥 ∈ 𝐵 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝐵) |
51 | | acsfn1 16145 |
. . . 4
⊢ ((𝐵 ∈ V ∧ ∀𝑥 ∈ 𝐵 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝐵) → {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦} ∈ (ACS‘𝐵)) |
52 | 38, 50, 51 | sylancr 694 |
. . 3
⊢ (𝑅 ∈ DivRing → {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦} ∈ (ACS‘𝐵)) |
53 | | mreincl 16082 |
. . 3
⊢
(((ACS‘𝐵)
∈ (Moore‘𝒫 𝐵) ∧ (SubRing‘𝑅) ∈ (ACS‘𝐵) ∧ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦} ∈ (ACS‘𝐵)) → ((SubRing‘𝑅) ∩ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦}) ∈ (ACS‘𝐵)) |
54 | 40, 43, 52, 53 | syl3anc 1318 |
. 2
⊢ (𝑅 ∈ DivRing →
((SubRing‘𝑅) ∩
{𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦}) ∈ (ACS‘𝐵)) |
55 | 36, 54 | eqeltrd 2688 |
1
⊢ (𝑅 ∈ DivRing →
(SubDRing‘𝑅) ∈
(ACS‘𝐵)) |