Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → 𝑅 ∈ RingOps) |
2 | | smprngpr.1 |
. . . . 5
⊢ 𝐺 = (1st ‘𝑅) |
3 | | smprngpr.4 |
. . . . 5
⊢ 𝑍 = (GId‘𝐺) |
4 | 2, 3 | 0idl 35795 |
. . . 4
⊢ (𝑅 ∈ RingOps → {𝑍} ∈ (Idl‘𝑅)) |
5 | 4 | 3ad2ant1 1134 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → {𝑍} ∈ (Idl‘𝑅)) |
6 | | smprngpr.2 |
. . . . . . . 8
⊢ 𝐻 = (2nd ‘𝑅) |
7 | | smprngpr.3 |
. . . . . . . 8
⊢ 𝑋 = ran 𝐺 |
8 | | smprngpr.5 |
. . . . . . . 8
⊢ 𝑈 = (GId‘𝐻) |
9 | 2, 6, 7, 3, 8 | 0rngo 35797 |
. . . . . . 7
⊢ (𝑅 ∈ RingOps → (𝑍 = 𝑈 ↔ 𝑋 = {𝑍})) |
10 | | eqcom 2745 |
. . . . . . 7
⊢ (𝑈 = 𝑍 ↔ 𝑍 = 𝑈) |
11 | | eqcom 2745 |
. . . . . . 7
⊢ ({𝑍} = 𝑋 ↔ 𝑋 = {𝑍}) |
12 | 9, 10, 11 | 3bitr4g 317 |
. . . . . 6
⊢ (𝑅 ∈ RingOps → (𝑈 = 𝑍 ↔ {𝑍} = 𝑋)) |
13 | 12 | necon3bid 2978 |
. . . . 5
⊢ (𝑅 ∈ RingOps → (𝑈 ≠ 𝑍 ↔ {𝑍} ≠ 𝑋)) |
14 | 13 | biimpa 480 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → {𝑍} ≠ 𝑋) |
15 | 14 | 3adant3 1133 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → {𝑍} ≠ 𝑋) |
16 | | df-pr 4516 |
. . . . . . . 8
⊢ {{𝑍}, 𝑋} = ({{𝑍}} ∪ {𝑋}) |
17 | 16 | eqeq2i 2751 |
. . . . . . 7
⊢
((Idl‘𝑅) =
{{𝑍}, 𝑋} ↔ (Idl‘𝑅) = ({{𝑍}} ∪ {𝑋})) |
18 | | eleq2 2821 |
. . . . . . . . 9
⊢
((Idl‘𝑅) =
({{𝑍}} ∪ {𝑋}) → (𝑖 ∈ (Idl‘𝑅) ↔ 𝑖 ∈ ({{𝑍}} ∪ {𝑋}))) |
19 | | eleq2 2821 |
. . . . . . . . 9
⊢
((Idl‘𝑅) =
({{𝑍}} ∪ {𝑋}) → (𝑗 ∈ (Idl‘𝑅) ↔ 𝑗 ∈ ({{𝑍}} ∪ {𝑋}))) |
20 | 18, 19 | anbi12d 634 |
. . . . . . . 8
⊢
((Idl‘𝑅) =
({{𝑍}} ∪ {𝑋}) → ((𝑖 ∈ (Idl‘𝑅) ∧ 𝑗 ∈ (Idl‘𝑅)) ↔ (𝑖 ∈ ({{𝑍}} ∪ {𝑋}) ∧ 𝑗 ∈ ({{𝑍}} ∪ {𝑋})))) |
21 | | elun 4037 |
. . . . . . . . . 10
⊢ (𝑖 ∈ ({{𝑍}} ∪ {𝑋}) ↔ (𝑖 ∈ {{𝑍}} ∨ 𝑖 ∈ {𝑋})) |
22 | | velsn 4529 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ {{𝑍}} ↔ 𝑖 = {𝑍}) |
23 | | velsn 4529 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ {𝑋} ↔ 𝑖 = 𝑋) |
24 | 22, 23 | orbi12i 914 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ {{𝑍}} ∨ 𝑖 ∈ {𝑋}) ↔ (𝑖 = {𝑍} ∨ 𝑖 = 𝑋)) |
25 | 21, 24 | bitri 278 |
. . . . . . . . 9
⊢ (𝑖 ∈ ({{𝑍}} ∪ {𝑋}) ↔ (𝑖 = {𝑍} ∨ 𝑖 = 𝑋)) |
26 | | elun 4037 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ({{𝑍}} ∪ {𝑋}) ↔ (𝑗 ∈ {{𝑍}} ∨ 𝑗 ∈ {𝑋})) |
27 | | velsn 4529 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ {{𝑍}} ↔ 𝑗 = {𝑍}) |
28 | | velsn 4529 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ {𝑋} ↔ 𝑗 = 𝑋) |
29 | 27, 28 | orbi12i 914 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ {{𝑍}} ∨ 𝑗 ∈ {𝑋}) ↔ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋)) |
30 | 26, 29 | bitri 278 |
. . . . . . . . 9
⊢ (𝑗 ∈ ({{𝑍}} ∪ {𝑋}) ↔ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋)) |
31 | 25, 30 | anbi12i 630 |
. . . . . . . 8
⊢ ((𝑖 ∈ ({{𝑍}} ∪ {𝑋}) ∧ 𝑗 ∈ ({{𝑍}} ∪ {𝑋})) ↔ ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋))) |
32 | 20, 31 | bitrdi 290 |
. . . . . . 7
⊢
((Idl‘𝑅) =
({{𝑍}} ∪ {𝑋}) → ((𝑖 ∈ (Idl‘𝑅) ∧ 𝑗 ∈ (Idl‘𝑅)) ↔ ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋)))) |
33 | 17, 32 | sylbi 220 |
. . . . . 6
⊢
((Idl‘𝑅) =
{{𝑍}, 𝑋} → ((𝑖 ∈ (Idl‘𝑅) ∧ 𝑗 ∈ (Idl‘𝑅)) ↔ ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋)))) |
34 | 33 | 3ad2ant3 1136 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → ((𝑖 ∈ (Idl‘𝑅) ∧ 𝑗 ∈ (Idl‘𝑅)) ↔ ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋)))) |
35 | | eqimss 3931 |
. . . . . . . . . . 11
⊢ (𝑖 = {𝑍} → 𝑖 ⊆ {𝑍}) |
36 | 35 | orcd 872 |
. . . . . . . . . 10
⊢ (𝑖 = {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})) |
37 | 36 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑖 = {𝑍} ∧ 𝑗 = {𝑍}) → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})) |
38 | 37 | a1d 25 |
. . . . . . . 8
⊢ ((𝑖 = {𝑍} ∧ 𝑗 = {𝑍}) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))) |
39 | 38 | a1i 11 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → ((𝑖 = {𝑍} ∧ 𝑗 = {𝑍}) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))) |
40 | | eqimss 3931 |
. . . . . . . . . . 11
⊢ (𝑗 = {𝑍} → 𝑗 ⊆ {𝑍}) |
41 | 40 | olcd 873 |
. . . . . . . . . 10
⊢ (𝑗 = {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})) |
42 | 41 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑖 = 𝑋 ∧ 𝑗 = {𝑍}) → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})) |
43 | 42 | a1d 25 |
. . . . . . . 8
⊢ ((𝑖 = 𝑋 ∧ 𝑗 = {𝑍}) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))) |
44 | 43 | a1i 11 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → ((𝑖 = 𝑋 ∧ 𝑗 = {𝑍}) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))) |
45 | 36 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑖 = {𝑍} ∧ 𝑗 = 𝑋) → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})) |
46 | 45 | a1d 25 |
. . . . . . . 8
⊢ ((𝑖 = {𝑍} ∧ 𝑗 = 𝑋) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))) |
47 | 46 | a1i 11 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → ((𝑖 = {𝑍} ∧ 𝑗 = 𝑋) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))) |
48 | 2 | rneqi 5774 |
. . . . . . . . . . . . . 14
⊢ ran 𝐺 = ran (1st
‘𝑅) |
49 | 7, 48 | eqtri 2761 |
. . . . . . . . . . . . 13
⊢ 𝑋 = ran (1st
‘𝑅) |
50 | 49, 6, 8 | rngo1cl 35709 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ RingOps → 𝑈 ∈ 𝑋) |
51 | 50 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → 𝑈 ∈ 𝑋) |
52 | 6, 49, 8 | rngolidm 35707 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ∈ 𝑋) → (𝑈𝐻𝑈) = 𝑈) |
53 | 50, 52 | mpdan 687 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ RingOps → (𝑈𝐻𝑈) = 𝑈) |
54 | 53 | eleq1d 2817 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ RingOps → ((𝑈𝐻𝑈) ∈ {𝑍} ↔ 𝑈 ∈ {𝑍})) |
55 | 8 | fvexi 6682 |
. . . . . . . . . . . . . . 15
⊢ 𝑈 ∈ V |
56 | 55 | elsn 4528 |
. . . . . . . . . . . . . 14
⊢ (𝑈 ∈ {𝑍} ↔ 𝑈 = 𝑍) |
57 | 54, 56 | bitrdi 290 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ RingOps → ((𝑈𝐻𝑈) ∈ {𝑍} ↔ 𝑈 = 𝑍)) |
58 | 57 | necon3bbid 2971 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ RingOps → (¬
(𝑈𝐻𝑈) ∈ {𝑍} ↔ 𝑈 ≠ 𝑍)) |
59 | 58 | biimpar 481 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → ¬ (𝑈𝐻𝑈) ∈ {𝑍}) |
60 | | oveq1 7171 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑈 → (𝑥𝐻𝑦) = (𝑈𝐻𝑦)) |
61 | 60 | eleq1d 2817 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑈 → ((𝑥𝐻𝑦) ∈ {𝑍} ↔ (𝑈𝐻𝑦) ∈ {𝑍})) |
62 | 61 | notbid 321 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑈 → (¬ (𝑥𝐻𝑦) ∈ {𝑍} ↔ ¬ (𝑈𝐻𝑦) ∈ {𝑍})) |
63 | | oveq2 7172 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑈 → (𝑈𝐻𝑦) = (𝑈𝐻𝑈)) |
64 | 63 | eleq1d 2817 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑈 → ((𝑈𝐻𝑦) ∈ {𝑍} ↔ (𝑈𝐻𝑈) ∈ {𝑍})) |
65 | 64 | notbid 321 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑈 → (¬ (𝑈𝐻𝑦) ∈ {𝑍} ↔ ¬ (𝑈𝐻𝑈) ∈ {𝑍})) |
66 | 62, 65 | rspc2ev 3536 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ 𝑋 ∧ 𝑈 ∈ 𝑋 ∧ ¬ (𝑈𝐻𝑈) ∈ {𝑍}) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ (𝑥𝐻𝑦) ∈ {𝑍}) |
67 | 51, 51, 59, 66 | syl3anc 1372 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ¬ (𝑥𝐻𝑦) ∈ {𝑍}) |
68 | | rexnal2 3169 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈
𝑋 ∃𝑦 ∈ 𝑋 ¬ (𝑥𝐻𝑦) ∈ {𝑍} ↔ ¬ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) ∈ {𝑍}) |
69 | 67, 68 | sylib 221 |
. . . . . . . . 9
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → ¬ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) ∈ {𝑍}) |
70 | 69 | pm2.21d 121 |
. . . . . . . 8
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))) |
71 | | raleq 3309 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑋 → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍})) |
72 | | raleq 3309 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑋 → (∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} ↔ ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) ∈ {𝑍})) |
73 | 72 | ralbidv 3109 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑋 → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) ∈ {𝑍})) |
74 | 71, 73 | sylan9bb 513 |
. . . . . . . . 9
⊢ ((𝑖 = 𝑋 ∧ 𝑗 = 𝑋) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) ∈ {𝑍})) |
75 | 74 | imbi1d 345 |
. . . . . . . 8
⊢ ((𝑖 = 𝑋 ∧ 𝑗 = 𝑋) → ((∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})) ↔ (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))) |
76 | 70, 75 | syl5ibrcom 250 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → ((𝑖 = 𝑋 ∧ 𝑗 = 𝑋) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))) |
77 | 39, 44, 47, 76 | ccased 1038 |
. . . . . 6
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍) → (((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋)) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))) |
78 | 77 | 3adant3 1133 |
. . . . 5
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → (((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋)) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))) |
79 | 34, 78 | sylbid 243 |
. . . 4
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → ((𝑖 ∈ (Idl‘𝑅) ∧ 𝑗 ∈ (Idl‘𝑅)) → (∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))) |
80 | 79 | ralrimivv 3102 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → ∀𝑖 ∈ (Idl‘𝑅)∀𝑗 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))) |
81 | 2, 6, 7 | ispridl 35804 |
. . . 4
⊢ (𝑅 ∈ RingOps → ({𝑍} ∈ (PrIdl‘𝑅) ↔ ({𝑍} ∈ (Idl‘𝑅) ∧ {𝑍} ≠ 𝑋 ∧ ∀𝑖 ∈ (Idl‘𝑅)∀𝑗 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))) |
82 | 81 | 3ad2ant1 1134 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → ({𝑍} ∈ (PrIdl‘𝑅) ↔ ({𝑍} ∈ (Idl‘𝑅) ∧ {𝑍} ≠ 𝑋 ∧ ∀𝑖 ∈ (Idl‘𝑅)∀𝑗 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑖 ∀𝑦 ∈ 𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))) |
83 | 5, 15, 80, 82 | mpbir3and 1343 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → {𝑍} ∈ (PrIdl‘𝑅)) |
84 | 2, 3 | isprrngo 35820 |
. 2
⊢ (𝑅 ∈ PrRing ↔ (𝑅 ∈ RingOps ∧ {𝑍} ∈ (PrIdl‘𝑅))) |
85 | 1, 83, 84 | sylanbrc 586 |
1
⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → 𝑅 ∈ PrRing) |