| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . . . . . . . 8
⊢
(invr‘𝑅) = (invr‘𝑅) | 
| 2 |  | eqid 2736 | . . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 3 | 1, 2 | issdrg2 20797 | . . . . . . 7
⊢ (𝑠 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ 𝑠 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠)) | 
| 4 |  | 3anass 1094 | . . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝑠 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠) ↔ (𝑅 ∈ DivRing ∧ (𝑠 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠))) | 
| 5 | 3, 4 | bitri 275 | . . . . . 6
⊢ (𝑠 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ (𝑠 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠))) | 
| 6 | 5 | baib 535 | . . . . 5
⊢ (𝑅 ∈ DivRing → (𝑠 ∈ (SubDRing‘𝑅) ↔ (𝑠 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠))) | 
| 7 |  | subrgacs.b | . . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑅) | 
| 8 | 7 | subrgss 20573 | . . . . . . . . 9
⊢ (𝑠 ∈ (SubRing‘𝑅) → 𝑠 ⊆ 𝐵) | 
| 9 |  | velpw 4604 | . . . . . . . . 9
⊢ (𝑠 ∈ 𝒫 𝐵 ↔ 𝑠 ⊆ 𝐵) | 
| 10 | 8, 9 | sylibr 234 | . . . . . . . 8
⊢ (𝑠 ∈ (SubRing‘𝑅) → 𝑠 ∈ 𝒫 𝐵) | 
| 11 | 10 | adantl 481 | . . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ 𝑠 ∈ (SubRing‘𝑅)) → 𝑠 ∈ 𝒫 𝐵) | 
| 12 |  | iftrue 4530 | . . . . . . . . . . . . . 14
⊢ (𝑥 = (0g‘𝑅) → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) = 𝑥) | 
| 13 | 12 | eleq1d 2825 | . . . . . . . . . . . . 13
⊢ (𝑥 = (0g‘𝑅) → (if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦 ↔ 𝑥 ∈ 𝑦)) | 
| 14 | 13 | biimprd 248 | . . . . . . . . . . . 12
⊢ (𝑥 = (0g‘𝑅) → (𝑥 ∈ 𝑦 → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦)) | 
| 15 |  | eldifsni 4789 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}) → 𝑥 ≠ (0g‘𝑅)) | 
| 16 | 15 | necon2bi 2970 | . . . . . . . . . . . . 13
⊢ (𝑥 = (0g‘𝑅) → ¬ 𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)})) | 
| 17 | 16 | pm2.21d 121 | . . . . . . . . . . . 12
⊢ (𝑥 = (0g‘𝑅) → (𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}) →
((invr‘𝑅)‘𝑥) ∈ 𝑦)) | 
| 18 | 14, 17 | 2thd 265 | . . . . . . . . . . 11
⊢ (𝑥 = (0g‘𝑅) → ((𝑥 ∈ 𝑦 → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦) ↔ (𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}) →
((invr‘𝑅)‘𝑥) ∈ 𝑦))) | 
| 19 |  | eldifsn 4785 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}) ↔ (𝑥 ∈ 𝑦 ∧ 𝑥 ≠ (0g‘𝑅))) | 
| 20 | 19 | rbaibr 537 | . . . . . . . . . . . 12
⊢ (𝑥 ≠ (0g‘𝑅) → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}))) | 
| 21 |  | ifnefalse 4536 | . . . . . . . . . . . . 13
⊢ (𝑥 ≠ (0g‘𝑅) → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) = ((invr‘𝑅)‘𝑥)) | 
| 22 | 21 | eleq1d 2825 | . . . . . . . . . . . 12
⊢ (𝑥 ≠ (0g‘𝑅) → (if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦 ↔ ((invr‘𝑅)‘𝑥) ∈ 𝑦)) | 
| 23 | 20, 22 | imbi12d 344 | . . . . . . . . . . 11
⊢ (𝑥 ≠ (0g‘𝑅) → ((𝑥 ∈ 𝑦 → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦) ↔ (𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}) →
((invr‘𝑅)‘𝑥) ∈ 𝑦))) | 
| 24 | 18, 23 | pm2.61ine 3024 | . . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑦 → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦) ↔ (𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)}) →
((invr‘𝑅)‘𝑥) ∈ 𝑦)) | 
| 25 | 24 | ralbii2 3088 | . . . . . . . . 9
⊢
(∀𝑥 ∈
𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦 ↔ ∀𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑦) | 
| 26 |  | difeq1 4118 | . . . . . . . . . 10
⊢ (𝑦 = 𝑠 → (𝑦 ∖ {(0g‘𝑅)}) = (𝑠 ∖ {(0g‘𝑅)})) | 
| 27 |  | eleq2w 2824 | . . . . . . . . . 10
⊢ (𝑦 = 𝑠 → (((invr‘𝑅)‘𝑥) ∈ 𝑦 ↔ ((invr‘𝑅)‘𝑥) ∈ 𝑠)) | 
| 28 | 26, 27 | raleqbidv 3345 | . . . . . . . . 9
⊢ (𝑦 = 𝑠 → (∀𝑥 ∈ (𝑦 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑦 ↔ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠)) | 
| 29 | 25, 28 | bitrid 283 | . . . . . . . 8
⊢ (𝑦 = 𝑠 → (∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦 ↔ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠)) | 
| 30 | 29 | elrab3 3692 | . . . . . . 7
⊢ (𝑠 ∈ 𝒫 𝐵 → (𝑠 ∈ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦} ↔ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠)) | 
| 31 | 11, 30 | syl 17 | . . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ 𝑠 ∈ (SubRing‘𝑅)) → (𝑠 ∈ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦} ↔ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠)) | 
| 32 | 31 | pm5.32da 579 | . . . . 5
⊢ (𝑅 ∈ DivRing → ((𝑠 ∈ (SubRing‘𝑅) ∧ 𝑠 ∈ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦}) ↔ (𝑠 ∈ (SubRing‘𝑅) ∧ ∀𝑥 ∈ (𝑠 ∖ {(0g‘𝑅)})((invr‘𝑅)‘𝑥) ∈ 𝑠))) | 
| 33 | 6, 32 | bitr4d 282 | . . . 4
⊢ (𝑅 ∈ DivRing → (𝑠 ∈ (SubDRing‘𝑅) ↔ (𝑠 ∈ (SubRing‘𝑅) ∧ 𝑠 ∈ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦}))) | 
| 34 |  | elin 3966 | . . . 4
⊢ (𝑠 ∈ ((SubRing‘𝑅) ∩ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦}) ↔ (𝑠 ∈ (SubRing‘𝑅) ∧ 𝑠 ∈ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦})) | 
| 35 | 33, 34 | bitr4di 289 | . . 3
⊢ (𝑅 ∈ DivRing → (𝑠 ∈ (SubDRing‘𝑅) ↔ 𝑠 ∈ ((SubRing‘𝑅) ∩ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦}))) | 
| 36 | 35 | eqrdv 2734 | . 2
⊢ (𝑅 ∈ DivRing →
(SubDRing‘𝑅) =
((SubRing‘𝑅) ∩
{𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦})) | 
| 37 | 7 | fvexi 6919 | . . . 4
⊢ 𝐵 ∈ V | 
| 38 |  | mreacs 17702 | . . . 4
⊢ (𝐵 ∈ V →
(ACS‘𝐵) ∈
(Moore‘𝒫 𝐵)) | 
| 39 | 37, 38 | mp1i 13 | . . 3
⊢ (𝑅 ∈ DivRing →
(ACS‘𝐵) ∈
(Moore‘𝒫 𝐵)) | 
| 40 |  | drngring 20737 | . . . 4
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) | 
| 41 | 7 | subrgacs 20802 | . . . 4
⊢ (𝑅 ∈ Ring →
(SubRing‘𝑅) ∈
(ACS‘𝐵)) | 
| 42 | 40, 41 | syl 17 | . . 3
⊢ (𝑅 ∈ DivRing →
(SubRing‘𝑅) ∈
(ACS‘𝐵)) | 
| 43 |  | simplr 768 | . . . . . 6
⊢ (((𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 = (0g‘𝑅)) → 𝑥 ∈ 𝐵) | 
| 44 |  | df-ne 2940 | . . . . . . 7
⊢ (𝑥 ≠ (0g‘𝑅) ↔ ¬ 𝑥 = (0g‘𝑅)) | 
| 45 | 7, 2, 1 | drnginvrcl 20754 | . . . . . . . 8
⊢ ((𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ (0g‘𝑅)) → ((invr‘𝑅)‘𝑥) ∈ 𝐵) | 
| 46 | 45 | 3expa 1118 | . . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ≠ (0g‘𝑅)) → ((invr‘𝑅)‘𝑥) ∈ 𝐵) | 
| 47 | 44, 46 | sylan2br 595 | . . . . . 6
⊢ (((𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵) ∧ ¬ 𝑥 = (0g‘𝑅)) → ((invr‘𝑅)‘𝑥) ∈ 𝐵) | 
| 48 | 43, 47 | ifclda 4560 | . . . . 5
⊢ ((𝑅 ∈ DivRing ∧ 𝑥 ∈ 𝐵) → if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝐵) | 
| 49 | 48 | ralrimiva 3145 | . . . 4
⊢ (𝑅 ∈ DivRing →
∀𝑥 ∈ 𝐵 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝐵) | 
| 50 |  | acsfn1 17705 | . . . 4
⊢ ((𝐵 ∈ V ∧ ∀𝑥 ∈ 𝐵 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝐵) → {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦} ∈ (ACS‘𝐵)) | 
| 51 | 37, 49, 50 | sylancr 587 | . . 3
⊢ (𝑅 ∈ DivRing → {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦} ∈ (ACS‘𝐵)) | 
| 52 |  | mreincl 17643 | . . 3
⊢
(((ACS‘𝐵)
∈ (Moore‘𝒫 𝐵) ∧ (SubRing‘𝑅) ∈ (ACS‘𝐵) ∧ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦} ∈ (ACS‘𝐵)) → ((SubRing‘𝑅) ∩ {𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦}) ∈ (ACS‘𝐵)) | 
| 53 | 39, 42, 51, 52 | syl3anc 1372 | . 2
⊢ (𝑅 ∈ DivRing →
((SubRing‘𝑅) ∩
{𝑦 ∈ 𝒫 𝐵 ∣ ∀𝑥 ∈ 𝑦 if(𝑥 = (0g‘𝑅), 𝑥, ((invr‘𝑅)‘𝑥)) ∈ 𝑦}) ∈ (ACS‘𝐵)) | 
| 54 | 36, 53 | eqeltrd 2840 | 1
⊢ (𝑅 ∈ DivRing →
(SubDRing‘𝑅) ∈
(ACS‘𝐵)) |