# Metamath Proof Explorer

## Theorem smprngopr

Description: A simple ring (one whose only ideals are 0 and R ) is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011)

Ref Expression
Hypotheses smprngpr.1 ${⊢}{G}={1}^{st}\left({R}\right)$
smprngpr.2 ${⊢}{H}={2}^{nd}\left({R}\right)$
smprngpr.3 ${⊢}{X}=\mathrm{ran}{G}$
smprngpr.4 ${⊢}{Z}=\mathrm{GId}\left({G}\right)$
smprngpr.5 ${⊢}{U}=\mathrm{GId}\left({H}\right)$
Assertion smprngopr ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\wedge \mathrm{Idl}\left({R}\right)=\left\{\left\{{Z}\right\},{X}\right\}\right)\to {R}\in \mathrm{PrRing}$

### Proof

Step Hyp Ref Expression
1 smprngpr.1 ${⊢}{G}={1}^{st}\left({R}\right)$
2 smprngpr.2 ${⊢}{H}={2}^{nd}\left({R}\right)$
3 smprngpr.3 ${⊢}{X}=\mathrm{ran}{G}$
4 smprngpr.4 ${⊢}{Z}=\mathrm{GId}\left({G}\right)$
5 smprngpr.5 ${⊢}{U}=\mathrm{GId}\left({H}\right)$
6 simp1 ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\wedge \mathrm{Idl}\left({R}\right)=\left\{\left\{{Z}\right\},{X}\right\}\right)\to {R}\in \mathrm{RingOps}$
7 1 4 0idl ${⊢}{R}\in \mathrm{RingOps}\to \left\{{Z}\right\}\in \mathrm{Idl}\left({R}\right)$
8 7 3ad2ant1 ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\wedge \mathrm{Idl}\left({R}\right)=\left\{\left\{{Z}\right\},{X}\right\}\right)\to \left\{{Z}\right\}\in \mathrm{Idl}\left({R}\right)$
9 1 2 3 4 5 0rngo ${⊢}{R}\in \mathrm{RingOps}\to \left({Z}={U}↔{X}=\left\{{Z}\right\}\right)$
10 eqcom ${⊢}{U}={Z}↔{Z}={U}$
11 eqcom ${⊢}\left\{{Z}\right\}={X}↔{X}=\left\{{Z}\right\}$
12 9 10 11 3bitr4g ${⊢}{R}\in \mathrm{RingOps}\to \left({U}={Z}↔\left\{{Z}\right\}={X}\right)$
13 12 necon3bid ${⊢}{R}\in \mathrm{RingOps}\to \left({U}\ne {Z}↔\left\{{Z}\right\}\ne {X}\right)$
14 13 biimpa ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\right)\to \left\{{Z}\right\}\ne {X}$
15 14 3adant3 ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\wedge \mathrm{Idl}\left({R}\right)=\left\{\left\{{Z}\right\},{X}\right\}\right)\to \left\{{Z}\right\}\ne {X}$
16 df-pr ${⊢}\left\{\left\{{Z}\right\},{X}\right\}=\left\{\left\{{Z}\right\}\right\}\cup \left\{{X}\right\}$
17 16 eqeq2i ${⊢}\mathrm{Idl}\left({R}\right)=\left\{\left\{{Z}\right\},{X}\right\}↔\mathrm{Idl}\left({R}\right)=\left\{\left\{{Z}\right\}\right\}\cup \left\{{X}\right\}$
18 eleq2 ${⊢}\mathrm{Idl}\left({R}\right)=\left\{\left\{{Z}\right\}\right\}\cup \left\{{X}\right\}\to \left({i}\in \mathrm{Idl}\left({R}\right)↔{i}\in \left(\left\{\left\{{Z}\right\}\right\}\cup \left\{{X}\right\}\right)\right)$
19 eleq2 ${⊢}\mathrm{Idl}\left({R}\right)=\left\{\left\{{Z}\right\}\right\}\cup \left\{{X}\right\}\to \left({j}\in \mathrm{Idl}\left({R}\right)↔{j}\in \left(\left\{\left\{{Z}\right\}\right\}\cup \left\{{X}\right\}\right)\right)$
20 18 19 anbi12d ${⊢}\mathrm{Idl}\left({R}\right)=\left\{\left\{{Z}\right\}\right\}\cup \left\{{X}\right\}\to \left(\left({i}\in \mathrm{Idl}\left({R}\right)\wedge {j}\in \mathrm{Idl}\left({R}\right)\right)↔\left({i}\in \left(\left\{\left\{{Z}\right\}\right\}\cup \left\{{X}\right\}\right)\wedge {j}\in \left(\left\{\left\{{Z}\right\}\right\}\cup \left\{{X}\right\}\right)\right)\right)$
21 elun ${⊢}{i}\in \left(\left\{\left\{{Z}\right\}\right\}\cup \left\{{X}\right\}\right)↔\left({i}\in \left\{\left\{{Z}\right\}\right\}\vee {i}\in \left\{{X}\right\}\right)$
22 velsn ${⊢}{i}\in \left\{\left\{{Z}\right\}\right\}↔{i}=\left\{{Z}\right\}$
23 velsn ${⊢}{i}\in \left\{{X}\right\}↔{i}={X}$
24 22 23 orbi12i ${⊢}\left({i}\in \left\{\left\{{Z}\right\}\right\}\vee {i}\in \left\{{X}\right\}\right)↔\left({i}=\left\{{Z}\right\}\vee {i}={X}\right)$
25 21 24 bitri ${⊢}{i}\in \left(\left\{\left\{{Z}\right\}\right\}\cup \left\{{X}\right\}\right)↔\left({i}=\left\{{Z}\right\}\vee {i}={X}\right)$
26 elun ${⊢}{j}\in \left(\left\{\left\{{Z}\right\}\right\}\cup \left\{{X}\right\}\right)↔\left({j}\in \left\{\left\{{Z}\right\}\right\}\vee {j}\in \left\{{X}\right\}\right)$
27 velsn ${⊢}{j}\in \left\{\left\{{Z}\right\}\right\}↔{j}=\left\{{Z}\right\}$
28 velsn ${⊢}{j}\in \left\{{X}\right\}↔{j}={X}$
29 27 28 orbi12i ${⊢}\left({j}\in \left\{\left\{{Z}\right\}\right\}\vee {j}\in \left\{{X}\right\}\right)↔\left({j}=\left\{{Z}\right\}\vee {j}={X}\right)$
30 26 29 bitri ${⊢}{j}\in \left(\left\{\left\{{Z}\right\}\right\}\cup \left\{{X}\right\}\right)↔\left({j}=\left\{{Z}\right\}\vee {j}={X}\right)$
31 25 30 anbi12i ${⊢}\left({i}\in \left(\left\{\left\{{Z}\right\}\right\}\cup \left\{{X}\right\}\right)\wedge {j}\in \left(\left\{\left\{{Z}\right\}\right\}\cup \left\{{X}\right\}\right)\right)↔\left(\left({i}=\left\{{Z}\right\}\vee {i}={X}\right)\wedge \left({j}=\left\{{Z}\right\}\vee {j}={X}\right)\right)$
32 20 31 syl6bb ${⊢}\mathrm{Idl}\left({R}\right)=\left\{\left\{{Z}\right\}\right\}\cup \left\{{X}\right\}\to \left(\left({i}\in \mathrm{Idl}\left({R}\right)\wedge {j}\in \mathrm{Idl}\left({R}\right)\right)↔\left(\left({i}=\left\{{Z}\right\}\vee {i}={X}\right)\wedge \left({j}=\left\{{Z}\right\}\vee {j}={X}\right)\right)\right)$
33 17 32 sylbi ${⊢}\mathrm{Idl}\left({R}\right)=\left\{\left\{{Z}\right\},{X}\right\}\to \left(\left({i}\in \mathrm{Idl}\left({R}\right)\wedge {j}\in \mathrm{Idl}\left({R}\right)\right)↔\left(\left({i}=\left\{{Z}\right\}\vee {i}={X}\right)\wedge \left({j}=\left\{{Z}\right\}\vee {j}={X}\right)\right)\right)$
34 33 3ad2ant3 ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\wedge \mathrm{Idl}\left({R}\right)=\left\{\left\{{Z}\right\},{X}\right\}\right)\to \left(\left({i}\in \mathrm{Idl}\left({R}\right)\wedge {j}\in \mathrm{Idl}\left({R}\right)\right)↔\left(\left({i}=\left\{{Z}\right\}\vee {i}={X}\right)\wedge \left({j}=\left\{{Z}\right\}\vee {j}={X}\right)\right)\right)$
35 eqimss ${⊢}{i}=\left\{{Z}\right\}\to {i}\subseteq \left\{{Z}\right\}$
36 35 orcd ${⊢}{i}=\left\{{Z}\right\}\to \left({i}\subseteq \left\{{Z}\right\}\vee {j}\subseteq \left\{{Z}\right\}\right)$
37 36 adantr ${⊢}\left({i}=\left\{{Z}\right\}\wedge {j}=\left\{{Z}\right\}\right)\to \left({i}\subseteq \left\{{Z}\right\}\vee {j}\subseteq \left\{{Z}\right\}\right)$
38 37 a1d ${⊢}\left({i}=\left\{{Z}\right\}\wedge {j}=\left\{{Z}\right\}\right)\to \left(\forall {x}\in {i}\phantom{\rule{.4em}{0ex}}\forall {y}\in {j}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}\to \left({i}\subseteq \left\{{Z}\right\}\vee {j}\subseteq \left\{{Z}\right\}\right)\right)$
39 38 a1i ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\right)\to \left(\left({i}=\left\{{Z}\right\}\wedge {j}=\left\{{Z}\right\}\right)\to \left(\forall {x}\in {i}\phantom{\rule{.4em}{0ex}}\forall {y}\in {j}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}\to \left({i}\subseteq \left\{{Z}\right\}\vee {j}\subseteq \left\{{Z}\right\}\right)\right)\right)$
40 eqimss ${⊢}{j}=\left\{{Z}\right\}\to {j}\subseteq \left\{{Z}\right\}$
41 40 olcd ${⊢}{j}=\left\{{Z}\right\}\to \left({i}\subseteq \left\{{Z}\right\}\vee {j}\subseteq \left\{{Z}\right\}\right)$
42 41 adantl ${⊢}\left({i}={X}\wedge {j}=\left\{{Z}\right\}\right)\to \left({i}\subseteq \left\{{Z}\right\}\vee {j}\subseteq \left\{{Z}\right\}\right)$
43 42 a1d ${⊢}\left({i}={X}\wedge {j}=\left\{{Z}\right\}\right)\to \left(\forall {x}\in {i}\phantom{\rule{.4em}{0ex}}\forall {y}\in {j}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}\to \left({i}\subseteq \left\{{Z}\right\}\vee {j}\subseteq \left\{{Z}\right\}\right)\right)$
44 43 a1i ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\right)\to \left(\left({i}={X}\wedge {j}=\left\{{Z}\right\}\right)\to \left(\forall {x}\in {i}\phantom{\rule{.4em}{0ex}}\forall {y}\in {j}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}\to \left({i}\subseteq \left\{{Z}\right\}\vee {j}\subseteq \left\{{Z}\right\}\right)\right)\right)$
45 36 adantr ${⊢}\left({i}=\left\{{Z}\right\}\wedge {j}={X}\right)\to \left({i}\subseteq \left\{{Z}\right\}\vee {j}\subseteq \left\{{Z}\right\}\right)$
46 45 a1d ${⊢}\left({i}=\left\{{Z}\right\}\wedge {j}={X}\right)\to \left(\forall {x}\in {i}\phantom{\rule{.4em}{0ex}}\forall {y}\in {j}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}\to \left({i}\subseteq \left\{{Z}\right\}\vee {j}\subseteq \left\{{Z}\right\}\right)\right)$
47 46 a1i ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\right)\to \left(\left({i}=\left\{{Z}\right\}\wedge {j}={X}\right)\to \left(\forall {x}\in {i}\phantom{\rule{.4em}{0ex}}\forall {y}\in {j}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}\to \left({i}\subseteq \left\{{Z}\right\}\vee {j}\subseteq \left\{{Z}\right\}\right)\right)\right)$
48 1 rneqi ${⊢}\mathrm{ran}{G}=\mathrm{ran}{1}^{st}\left({R}\right)$
49 3 48 eqtri ${⊢}{X}=\mathrm{ran}{1}^{st}\left({R}\right)$
50 49 2 5 rngo1cl ${⊢}{R}\in \mathrm{RingOps}\to {U}\in {X}$
51 50 adantr ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\right)\to {U}\in {X}$
52 2 49 5 rngolidm ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\in {X}\right)\to {U}{H}{U}={U}$
53 50 52 mpdan ${⊢}{R}\in \mathrm{RingOps}\to {U}{H}{U}={U}$
54 53 eleq1d ${⊢}{R}\in \mathrm{RingOps}\to \left({U}{H}{U}\in \left\{{Z}\right\}↔{U}\in \left\{{Z}\right\}\right)$
55 5 fvexi ${⊢}{U}\in \mathrm{V}$
56 55 elsn ${⊢}{U}\in \left\{{Z}\right\}↔{U}={Z}$
57 54 56 syl6bb ${⊢}{R}\in \mathrm{RingOps}\to \left({U}{H}{U}\in \left\{{Z}\right\}↔{U}={Z}\right)$
58 57 necon3bbid ${⊢}{R}\in \mathrm{RingOps}\to \left(¬{U}{H}{U}\in \left\{{Z}\right\}↔{U}\ne {Z}\right)$
59 58 biimpar ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\right)\to ¬{U}{H}{U}\in \left\{{Z}\right\}$
60 oveq1 ${⊢}{x}={U}\to {x}{H}{y}={U}{H}{y}$
61 60 eleq1d ${⊢}{x}={U}\to \left({x}{H}{y}\in \left\{{Z}\right\}↔{U}{H}{y}\in \left\{{Z}\right\}\right)$
62 61 notbid ${⊢}{x}={U}\to \left(¬{x}{H}{y}\in \left\{{Z}\right\}↔¬{U}{H}{y}\in \left\{{Z}\right\}\right)$
63 oveq2 ${⊢}{y}={U}\to {U}{H}{y}={U}{H}{U}$
64 63 eleq1d ${⊢}{y}={U}\to \left({U}{H}{y}\in \left\{{Z}\right\}↔{U}{H}{U}\in \left\{{Z}\right\}\right)$
65 64 notbid ${⊢}{y}={U}\to \left(¬{U}{H}{y}\in \left\{{Z}\right\}↔¬{U}{H}{U}\in \left\{{Z}\right\}\right)$
66 62 65 rspc2ev ${⊢}\left({U}\in {X}\wedge {U}\in {X}\wedge ¬{U}{H}{U}\in \left\{{Z}\right\}\right)\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}¬{x}{H}{y}\in \left\{{Z}\right\}$
67 51 51 59 66 syl3anc ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\right)\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}¬{x}{H}{y}\in \left\{{Z}\right\}$
68 rexnal2 ${⊢}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\exists {y}\in {X}\phantom{\rule{.4em}{0ex}}¬{x}{H}{y}\in \left\{{Z}\right\}↔¬\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}$
69 67 68 sylib ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\right)\to ¬\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}$
70 69 pm2.21d ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}\to \left({i}\subseteq \left\{{Z}\right\}\vee {j}\subseteq \left\{{Z}\right\}\right)\right)$
71 raleq ${⊢}{i}={X}\to \left(\forall {x}\in {i}\phantom{\rule{.4em}{0ex}}\forall {y}\in {j}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {j}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}\right)$
72 raleq ${⊢}{j}={X}\to \left(\forall {y}\in {j}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}\right)$
73 72 ralbidv ${⊢}{j}={X}\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {j}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}\right)$
74 71 73 sylan9bb ${⊢}\left({i}={X}\wedge {j}={X}\right)\to \left(\forall {x}\in {i}\phantom{\rule{.4em}{0ex}}\forall {y}\in {j}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}\right)$
75 74 imbi1d ${⊢}\left({i}={X}\wedge {j}={X}\right)\to \left(\left(\forall {x}\in {i}\phantom{\rule{.4em}{0ex}}\forall {y}\in {j}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}\to \left({i}\subseteq \left\{{Z}\right\}\vee {j}\subseteq \left\{{Z}\right\}\right)\right)↔\left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}\to \left({i}\subseteq \left\{{Z}\right\}\vee {j}\subseteq \left\{{Z}\right\}\right)\right)\right)$
76 70 75 syl5ibrcom ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\right)\to \left(\left({i}={X}\wedge {j}={X}\right)\to \left(\forall {x}\in {i}\phantom{\rule{.4em}{0ex}}\forall {y}\in {j}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}\to \left({i}\subseteq \left\{{Z}\right\}\vee {j}\subseteq \left\{{Z}\right\}\right)\right)\right)$
77 39 44 47 76 ccased ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\right)\to \left(\left(\left({i}=\left\{{Z}\right\}\vee {i}={X}\right)\wedge \left({j}=\left\{{Z}\right\}\vee {j}={X}\right)\right)\to \left(\forall {x}\in {i}\phantom{\rule{.4em}{0ex}}\forall {y}\in {j}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}\to \left({i}\subseteq \left\{{Z}\right\}\vee {j}\subseteq \left\{{Z}\right\}\right)\right)\right)$
78 77 3adant3 ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\wedge \mathrm{Idl}\left({R}\right)=\left\{\left\{{Z}\right\},{X}\right\}\right)\to \left(\left(\left({i}=\left\{{Z}\right\}\vee {i}={X}\right)\wedge \left({j}=\left\{{Z}\right\}\vee {j}={X}\right)\right)\to \left(\forall {x}\in {i}\phantom{\rule{.4em}{0ex}}\forall {y}\in {j}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}\to \left({i}\subseteq \left\{{Z}\right\}\vee {j}\subseteq \left\{{Z}\right\}\right)\right)\right)$
79 34 78 sylbid ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\wedge \mathrm{Idl}\left({R}\right)=\left\{\left\{{Z}\right\},{X}\right\}\right)\to \left(\left({i}\in \mathrm{Idl}\left({R}\right)\wedge {j}\in \mathrm{Idl}\left({R}\right)\right)\to \left(\forall {x}\in {i}\phantom{\rule{.4em}{0ex}}\forall {y}\in {j}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}\to \left({i}\subseteq \left\{{Z}\right\}\vee {j}\subseteq \left\{{Z}\right\}\right)\right)\right)$
80 79 ralrimivv ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\wedge \mathrm{Idl}\left({R}\right)=\left\{\left\{{Z}\right\},{X}\right\}\right)\to \forall {i}\in \mathrm{Idl}\left({R}\right)\phantom{\rule{.4em}{0ex}}\forall {j}\in \mathrm{Idl}\left({R}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {i}\phantom{\rule{.4em}{0ex}}\forall {y}\in {j}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}\to \left({i}\subseteq \left\{{Z}\right\}\vee {j}\subseteq \left\{{Z}\right\}\right)\right)$
81 1 2 3 ispridl ${⊢}{R}\in \mathrm{RingOps}\to \left(\left\{{Z}\right\}\in \mathrm{PrIdl}\left({R}\right)↔\left(\left\{{Z}\right\}\in \mathrm{Idl}\left({R}\right)\wedge \left\{{Z}\right\}\ne {X}\wedge \forall {i}\in \mathrm{Idl}\left({R}\right)\phantom{\rule{.4em}{0ex}}\forall {j}\in \mathrm{Idl}\left({R}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {i}\phantom{\rule{.4em}{0ex}}\forall {y}\in {j}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}\to \left({i}\subseteq \left\{{Z}\right\}\vee {j}\subseteq \left\{{Z}\right\}\right)\right)\right)\right)$
82 81 3ad2ant1 ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\wedge \mathrm{Idl}\left({R}\right)=\left\{\left\{{Z}\right\},{X}\right\}\right)\to \left(\left\{{Z}\right\}\in \mathrm{PrIdl}\left({R}\right)↔\left(\left\{{Z}\right\}\in \mathrm{Idl}\left({R}\right)\wedge \left\{{Z}\right\}\ne {X}\wedge \forall {i}\in \mathrm{Idl}\left({R}\right)\phantom{\rule{.4em}{0ex}}\forall {j}\in \mathrm{Idl}\left({R}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {i}\phantom{\rule{.4em}{0ex}}\forall {y}\in {j}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \left\{{Z}\right\}\to \left({i}\subseteq \left\{{Z}\right\}\vee {j}\subseteq \left\{{Z}\right\}\right)\right)\right)\right)$
83 8 15 80 82 mpbir3and ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\wedge \mathrm{Idl}\left({R}\right)=\left\{\left\{{Z}\right\},{X}\right\}\right)\to \left\{{Z}\right\}\in \mathrm{PrIdl}\left({R}\right)$
84 1 4 isprrngo ${⊢}{R}\in \mathrm{PrRing}↔\left({R}\in \mathrm{RingOps}\wedge \left\{{Z}\right\}\in \mathrm{PrIdl}\left({R}\right)\right)$
85 6 83 84 sylanbrc ${⊢}\left({R}\in \mathrm{RingOps}\wedge {U}\ne {Z}\wedge \mathrm{Idl}\left({R}\right)=\left\{\left\{{Z}\right\},{X}\right\}\right)\to {R}\in \mathrm{PrRing}$