Step | Hyp | Ref
| Expression |
1 | | 0idl.1 |
. . . 4
⊢ 𝐺 = (1st ‘𝑅) |
2 | | eqid 2622 |
. . . 4
⊢ ran 𝐺 = ran 𝐺 |
3 | | 0idl.2 |
. . . 4
⊢ 𝑍 = (GId‘𝐺) |
4 | 1, 2, 3 | rngo0cl 33718 |
. . 3
⊢ (𝑅 ∈ RingOps → 𝑍 ∈ ran 𝐺) |
5 | 4 | snssd 4340 |
. 2
⊢ (𝑅 ∈ RingOps → {𝑍} ⊆ ran 𝐺) |
6 | | fvex 6201 |
. . . . 5
⊢
(GId‘𝐺) ∈
V |
7 | 3, 6 | eqeltri 2697 |
. . . 4
⊢ 𝑍 ∈ V |
8 | 7 | snid 4208 |
. . 3
⊢ 𝑍 ∈ {𝑍} |
9 | 8 | a1i 11 |
. 2
⊢ (𝑅 ∈ RingOps → 𝑍 ∈ {𝑍}) |
10 | | velsn 4193 |
. . . 4
⊢ (𝑥 ∈ {𝑍} ↔ 𝑥 = 𝑍) |
11 | | velsn 4193 |
. . . . . . . 8
⊢ (𝑦 ∈ {𝑍} ↔ 𝑦 = 𝑍) |
12 | 1, 2, 3 | rngo0rid 33719 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ RingOps ∧ 𝑍 ∈ ran 𝐺) → (𝑍𝐺𝑍) = 𝑍) |
13 | 4, 12 | mpdan 702 |
. . . . . . . . . 10
⊢ (𝑅 ∈ RingOps → (𝑍𝐺𝑍) = 𝑍) |
14 | | ovex 6678 |
. . . . . . . . . . 11
⊢ (𝑍𝐺𝑍) ∈ V |
15 | 14 | elsn 4192 |
. . . . . . . . . 10
⊢ ((𝑍𝐺𝑍) ∈ {𝑍} ↔ (𝑍𝐺𝑍) = 𝑍) |
16 | 13, 15 | sylibr 224 |
. . . . . . . . 9
⊢ (𝑅 ∈ RingOps → (𝑍𝐺𝑍) ∈ {𝑍}) |
17 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑍 → (𝑍𝐺𝑦) = (𝑍𝐺𝑍)) |
18 | 17 | eleq1d 2686 |
. . . . . . . . 9
⊢ (𝑦 = 𝑍 → ((𝑍𝐺𝑦) ∈ {𝑍} ↔ (𝑍𝐺𝑍) ∈ {𝑍})) |
19 | 16, 18 | syl5ibrcom 237 |
. . . . . . . 8
⊢ (𝑅 ∈ RingOps → (𝑦 = 𝑍 → (𝑍𝐺𝑦) ∈ {𝑍})) |
20 | 11, 19 | syl5bi 232 |
. . . . . . 7
⊢ (𝑅 ∈ RingOps → (𝑦 ∈ {𝑍} → (𝑍𝐺𝑦) ∈ {𝑍})) |
21 | 20 | ralrimiv 2965 |
. . . . . 6
⊢ (𝑅 ∈ RingOps →
∀𝑦 ∈ {𝑍} (𝑍𝐺𝑦) ∈ {𝑍}) |
22 | | eqid 2622 |
. . . . . . . . . 10
⊢
(2nd ‘𝑅) = (2nd ‘𝑅) |
23 | 3, 2, 1, 22 | rngorz 33722 |
. . . . . . . . 9
⊢ ((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran 𝐺) → (𝑧(2nd ‘𝑅)𝑍) = 𝑍) |
24 | | ovex 6678 |
. . . . . . . . . 10
⊢ (𝑧(2nd ‘𝑅)𝑍) ∈ V |
25 | 24 | elsn 4192 |
. . . . . . . . 9
⊢ ((𝑧(2nd ‘𝑅)𝑍) ∈ {𝑍} ↔ (𝑧(2nd ‘𝑅)𝑍) = 𝑍) |
26 | 23, 25 | sylibr 224 |
. . . . . . . 8
⊢ ((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran 𝐺) → (𝑧(2nd ‘𝑅)𝑍) ∈ {𝑍}) |
27 | 3, 2, 1, 22 | rngolz 33721 |
. . . . . . . . 9
⊢ ((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran 𝐺) → (𝑍(2nd ‘𝑅)𝑧) = 𝑍) |
28 | | ovex 6678 |
. . . . . . . . . 10
⊢ (𝑍(2nd ‘𝑅)𝑧) ∈ V |
29 | 28 | elsn 4192 |
. . . . . . . . 9
⊢ ((𝑍(2nd ‘𝑅)𝑧) ∈ {𝑍} ↔ (𝑍(2nd ‘𝑅)𝑧) = 𝑍) |
30 | 27, 29 | sylibr 224 |
. . . . . . . 8
⊢ ((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran 𝐺) → (𝑍(2nd ‘𝑅)𝑧) ∈ {𝑍}) |
31 | 26, 30 | jca 554 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran 𝐺) → ((𝑧(2nd ‘𝑅)𝑍) ∈ {𝑍} ∧ (𝑍(2nd ‘𝑅)𝑧) ∈ {𝑍})) |
32 | 31 | ralrimiva 2966 |
. . . . . 6
⊢ (𝑅 ∈ RingOps →
∀𝑧 ∈ ran 𝐺((𝑧(2nd ‘𝑅)𝑍) ∈ {𝑍} ∧ (𝑍(2nd ‘𝑅)𝑧) ∈ {𝑍})) |
33 | 21, 32 | jca 554 |
. . . . 5
⊢ (𝑅 ∈ RingOps →
(∀𝑦 ∈ {𝑍} (𝑍𝐺𝑦) ∈ {𝑍} ∧ ∀𝑧 ∈ ran 𝐺((𝑧(2nd ‘𝑅)𝑍) ∈ {𝑍} ∧ (𝑍(2nd ‘𝑅)𝑧) ∈ {𝑍}))) |
34 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑥 = 𝑍 → (𝑥𝐺𝑦) = (𝑍𝐺𝑦)) |
35 | 34 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑥 = 𝑍 → ((𝑥𝐺𝑦) ∈ {𝑍} ↔ (𝑍𝐺𝑦) ∈ {𝑍})) |
36 | 35 | ralbidv 2986 |
. . . . . 6
⊢ (𝑥 = 𝑍 → (∀𝑦 ∈ {𝑍} (𝑥𝐺𝑦) ∈ {𝑍} ↔ ∀𝑦 ∈ {𝑍} (𝑍𝐺𝑦) ∈ {𝑍})) |
37 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑥 = 𝑍 → (𝑧(2nd ‘𝑅)𝑥) = (𝑧(2nd ‘𝑅)𝑍)) |
38 | 37 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑥 = 𝑍 → ((𝑧(2nd ‘𝑅)𝑥) ∈ {𝑍} ↔ (𝑧(2nd ‘𝑅)𝑍) ∈ {𝑍})) |
39 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑥 = 𝑍 → (𝑥(2nd ‘𝑅)𝑧) = (𝑍(2nd ‘𝑅)𝑧)) |
40 | 39 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑥 = 𝑍 → ((𝑥(2nd ‘𝑅)𝑧) ∈ {𝑍} ↔ (𝑍(2nd ‘𝑅)𝑧) ∈ {𝑍})) |
41 | 38, 40 | anbi12d 747 |
. . . . . . 7
⊢ (𝑥 = 𝑍 → (((𝑧(2nd ‘𝑅)𝑥) ∈ {𝑍} ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ {𝑍}) ↔ ((𝑧(2nd ‘𝑅)𝑍) ∈ {𝑍} ∧ (𝑍(2nd ‘𝑅)𝑧) ∈ {𝑍}))) |
42 | 41 | ralbidv 2986 |
. . . . . 6
⊢ (𝑥 = 𝑍 → (∀𝑧 ∈ ran 𝐺((𝑧(2nd ‘𝑅)𝑥) ∈ {𝑍} ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ {𝑍}) ↔ ∀𝑧 ∈ ran 𝐺((𝑧(2nd ‘𝑅)𝑍) ∈ {𝑍} ∧ (𝑍(2nd ‘𝑅)𝑧) ∈ {𝑍}))) |
43 | 36, 42 | anbi12d 747 |
. . . . 5
⊢ (𝑥 = 𝑍 → ((∀𝑦 ∈ {𝑍} (𝑥𝐺𝑦) ∈ {𝑍} ∧ ∀𝑧 ∈ ran 𝐺((𝑧(2nd ‘𝑅)𝑥) ∈ {𝑍} ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ {𝑍})) ↔ (∀𝑦 ∈ {𝑍} (𝑍𝐺𝑦) ∈ {𝑍} ∧ ∀𝑧 ∈ ran 𝐺((𝑧(2nd ‘𝑅)𝑍) ∈ {𝑍} ∧ (𝑍(2nd ‘𝑅)𝑧) ∈ {𝑍})))) |
44 | 33, 43 | syl5ibrcom 237 |
. . . 4
⊢ (𝑅 ∈ RingOps → (𝑥 = 𝑍 → (∀𝑦 ∈ {𝑍} (𝑥𝐺𝑦) ∈ {𝑍} ∧ ∀𝑧 ∈ ran 𝐺((𝑧(2nd ‘𝑅)𝑥) ∈ {𝑍} ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ {𝑍})))) |
45 | 10, 44 | syl5bi 232 |
. . 3
⊢ (𝑅 ∈ RingOps → (𝑥 ∈ {𝑍} → (∀𝑦 ∈ {𝑍} (𝑥𝐺𝑦) ∈ {𝑍} ∧ ∀𝑧 ∈ ran 𝐺((𝑧(2nd ‘𝑅)𝑥) ∈ {𝑍} ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ {𝑍})))) |
46 | 45 | ralrimiv 2965 |
. 2
⊢ (𝑅 ∈ RingOps →
∀𝑥 ∈ {𝑍} (∀𝑦 ∈ {𝑍} (𝑥𝐺𝑦) ∈ {𝑍} ∧ ∀𝑧 ∈ ran 𝐺((𝑧(2nd ‘𝑅)𝑥) ∈ {𝑍} ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ {𝑍}))) |
47 | 1, 22, 2, 3 | isidl 33813 |
. 2
⊢ (𝑅 ∈ RingOps → ({𝑍} ∈ (Idl‘𝑅) ↔ ({𝑍} ⊆ ran 𝐺 ∧ 𝑍 ∈ {𝑍} ∧ ∀𝑥 ∈ {𝑍} (∀𝑦 ∈ {𝑍} (𝑥𝐺𝑦) ∈ {𝑍} ∧ ∀𝑧 ∈ ran 𝐺((𝑧(2nd ‘𝑅)𝑥) ∈ {𝑍} ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ {𝑍}))))) |
48 | 5, 9, 46, 47 | mpbir3and 1245 |
1
⊢ (𝑅 ∈ RingOps → {𝑍} ∈ (Idl‘𝑅)) |