Metamath Proof Explorer

Theorem smprngprmrng

Description: A simple ring (a nonzero ring whose only ideals are .0. and R ) is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011) (Revised by AV, 18-Jun-2026)

Ref Expression
Hypotheses smprngprmrng.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
smprngprmrng.z ⊢ 0 = ( 0g ‘ 𝑅 )
smprngprmrng.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
Assertion smprngprmrng ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) → 𝑅 ∈ PrmRing )

Proof

Step Hyp Ref Expression
1 smprngprmrng.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 smprngprmrng.z ⊢ 0 = ( 0g ‘ 𝑅 )
3 smprngprmrng.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
4 nzrring ⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
5 4 adantr ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) → 𝑅 ∈ Ring )
6 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
7 6 2 lidl0 ⊢ ( 𝑅 ∈ Ring → { 0 } ∈ ( LIdeal ‘ 𝑅 ) )
8 4 7 syl ⊢ ( 𝑅 ∈ NzRing → { 0 } ∈ ( LIdeal ‘ 𝑅 ) )
9 8 adantr ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) → { 0 } ∈ ( LIdeal ‘ 𝑅 ) )
10 2 1 drnglidl1ne0 ⊢ ( 𝑅 ∈ NzRing → 𝐵 ≠ { 0 } )
11 10 necomd ⊢ ( 𝑅 ∈ NzRing → { 0 } ≠ 𝐵 )
12 11 adantr ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) → { 0 } ≠ 𝐵 )
13 df-pr ⊢ { { 0 } , 𝐵 } = ( { { 0 } } ∪ { 𝐵 } )
14 13 eqeq2i ⊢ ( 𝑈 = { { 0 } , 𝐵 } ↔ 𝑈 = ( { { 0 } } ∪ { 𝐵 } ) )
15 id ⊢ ( 𝑈 = ( { { 0 } } ∪ { 𝐵 } ) → 𝑈 = ( { { 0 } } ∪ { 𝐵 } ) )
16 3 15 eqtr3id ⊢ ( 𝑈 = ( { { 0 } } ∪ { 𝐵 } ) → ( LIdeal ‘ 𝑅 ) = ( { { 0 } } ∪ { 𝐵 } ) )
17 16 eleq2d ⊢ ( 𝑈 = ( { { 0 } } ∪ { 𝐵 } ) → ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ↔ 𝑎 ∈ ( { { 0 } } ∪ { 𝐵 } ) ) )
18 16 eleq2d ⊢ ( 𝑈 = ( { { 0 } } ∪ { 𝐵 } ) → ( 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ↔ 𝑏 ∈ ( { { 0 } } ∪ { 𝐵 } ) ) )
19 17 18 anbi12d ⊢ ( 𝑈 = ( { { 0 } } ∪ { 𝐵 } ) → ( ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ↔ ( 𝑎 ∈ ( { { 0 } } ∪ { 𝐵 } ) ∧ 𝑏 ∈ ( { { 0 } } ∪ { 𝐵 } ) ) ) )
20 elun ⊢ ( 𝑎 ∈ ( { { 0 } } ∪ { 𝐵 } ) ↔ ( 𝑎 ∈ { { 0 } } ∨ 𝑎 ∈ { 𝐵 } ) )
21 velsn ⊢ ( 𝑎 ∈ { { 0 } } ↔ 𝑎 = { 0 } )
22 velsn ⊢ ( 𝑎 ∈ { 𝐵 } ↔ 𝑎 = 𝐵 )
23 21 22 orbi12i ⊢ ( ( 𝑎 ∈ { { 0 } } ∨ 𝑎 ∈ { 𝐵 } ) ↔ ( 𝑎 = { 0 } ∨ 𝑎 = 𝐵 ) )
24 20 23 bitri ⊢ ( 𝑎 ∈ ( { { 0 } } ∪ { 𝐵 } ) ↔ ( 𝑎 = { 0 } ∨ 𝑎 = 𝐵 ) )
25 elun ⊢ ( 𝑏 ∈ ( { { 0 } } ∪ { 𝐵 } ) ↔ ( 𝑏 ∈ { { 0 } } ∨ 𝑏 ∈ { 𝐵 } ) )
26 velsn ⊢ ( 𝑏 ∈ { { 0 } } ↔ 𝑏 = { 0 } )
27 velsn ⊢ ( 𝑏 ∈ { 𝐵 } ↔ 𝑏 = 𝐵 )
28 26 27 orbi12i ⊢ ( ( 𝑏 ∈ { { 0 } } ∨ 𝑏 ∈ { 𝐵 } ) ↔ ( 𝑏 = { 0 } ∨ 𝑏 = 𝐵 ) )
29 25 28 bitri ⊢ ( 𝑏 ∈ ( { { 0 } } ∪ { 𝐵 } ) ↔ ( 𝑏 = { 0 } ∨ 𝑏 = 𝐵 ) )
30 24 29 anbi12i ⊢ ( ( 𝑎 ∈ ( { { 0 } } ∪ { 𝐵 } ) ∧ 𝑏 ∈ ( { { 0 } } ∪ { 𝐵 } ) ) ↔ ( ( 𝑎 = { 0 } ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = { 0 } ∨ 𝑏 = 𝐵 ) ) )
31 19 30 bitrdi ⊢ ( 𝑈 = ( { { 0 } } ∪ { 𝐵 } ) → ( ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ↔ ( ( 𝑎 = { 0 } ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = { 0 } ∨ 𝑏 = 𝐵 ) ) ) )
32 14 31 sylbi ⊢ ( 𝑈 = { { 0 } , 𝐵 } → ( ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ↔ ( ( 𝑎 = { 0 } ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = { 0 } ∨ 𝑏 = 𝐵 ) ) ) )
33 32 adantl ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) → ( ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) ↔ ( ( 𝑎 = { 0 } ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = { 0 } ∨ 𝑏 = 𝐵 ) ) ) )
34 eqimss ⊢ ( 𝑎 = { 0 } → 𝑎 ⊆ { 0 } )
35 34 orcd ⊢ ( 𝑎 = { 0 } → ( 𝑎 ⊆ { 0 } ∨ 𝑏 ⊆ { 0 } ) )
36 35 adantr ⊢ ( ( 𝑎 = { 0 } ∧ 𝑏 = { 0 } ) → ( 𝑎 ⊆ { 0 } ∨ 𝑏 ⊆ { 0 } ) )
37 36 a1i13 ⊢ ( 𝑅 ∈ NzRing → ( ( 𝑎 = { 0 } ∧ 𝑏 = { 0 } ) → ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } → ( 𝑎 ⊆ { 0 } ∨ 𝑏 ⊆ { 0 } ) ) ) )
38 eqimss ⊢ ( 𝑏 = { 0 } → 𝑏 ⊆ { 0 } )
39 38 olcd ⊢ ( 𝑏 = { 0 } → ( 𝑎 ⊆ { 0 } ∨ 𝑏 ⊆ { 0 } ) )
40 39 adantl ⊢ ( ( 𝑎 = 𝐵 ∧ 𝑏 = { 0 } ) → ( 𝑎 ⊆ { 0 } ∨ 𝑏 ⊆ { 0 } ) )
41 40 a1i13 ⊢ ( 𝑅 ∈ NzRing → ( ( 𝑎 = 𝐵 ∧ 𝑏 = { 0 } ) → ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } → ( 𝑎 ⊆ { 0 } ∨ 𝑏 ⊆ { 0 } ) ) ) )
42 35 adantr ⊢ ( ( 𝑎 = { 0 } ∧ 𝑏 = 𝐵 ) → ( 𝑎 ⊆ { 0 } ∨ 𝑏 ⊆ { 0 } ) )
43 42 a1i13 ⊢ ( 𝑅 ∈ NzRing → ( ( 𝑎 = { 0 } ∧ 𝑏 = 𝐵 ) → ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } → ( 𝑎 ⊆ { 0 } ∨ 𝑏 ⊆ { 0 } ) ) ) )
44 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
45 1 44 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
46 4 45 syl ⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
47 44 2 nzrnz ⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ 0 )
48 47 neneqd ⊢ ( 𝑅 ∈ NzRing → ¬ ( 1r ‘ 𝑅 ) = 0 )
49 ringsrg ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ SRing )
50 49 45 jca ⊢ ( 𝑅 ∈ Ring → ( 𝑅 ∈ SRing ∧ ( 1r ‘ 𝑅 ) ∈ 𝐵 ) )
51 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
52 1 51 44 srgridm ⊢ ( ( 𝑅 ∈ SRing ∧ ( 1r ‘ 𝑅 ) ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
53 4 50 52 3syl ⊢ ( 𝑅 ∈ NzRing → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
54 53 eqeq1d ⊢ ( 𝑅 ∈ NzRing → ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 0 ↔ ( 1r ‘ 𝑅 ) = 0 ) )
55 48 54 mtbird ⊢ ( 𝑅 ∈ NzRing → ¬ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 0 )
56 ovex ⊢ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ∈ V
57 56 elsn ⊢ ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ∈ { 0 } ↔ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 0 )
58 55 57 sylnibr ⊢ ( 𝑅 ∈ NzRing → ¬ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ∈ { 0 } )
59 oveq1 ⊢ ( 𝑥 = ( 1r ‘ 𝑅 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑦 ) )
60 59 eleq1d ⊢ ( 𝑥 = ( 1r ‘ 𝑅 ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } ↔ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } ) )
61 60 notbid ⊢ ( 𝑥 = ( 1r ‘ 𝑅 ) → ( ¬ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } ↔ ¬ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } ) )
62 oveq2 ⊢ ( 𝑦 = ( 1r ‘ 𝑅 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑦 ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
63 62 eleq1d ⊢ ( 𝑦 = ( 1r ‘ 𝑅 ) → ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } ↔ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ∈ { 0 } ) )
64 63 notbid ⊢ ( 𝑦 = ( 1r ‘ 𝑅 ) → ( ¬ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } ↔ ¬ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ∈ { 0 } ) )
65 61 64 rspc2ev ⊢ ( ( ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ¬ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ∈ { 0 } ) → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ¬ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } )
66 46 46 58 65 syl3anc ⊢ ( 𝑅 ∈ NzRing → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ¬ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } )
67 rexnal2 ⊢ ( ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ¬ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } ↔ ¬ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } )
68 66 67 sylib ⊢ ( 𝑅 ∈ NzRing → ¬ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } )
69 68 pm2.21d ⊢ ( 𝑅 ∈ NzRing → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } → ( 𝑎 ⊆ { 0 } ∨ 𝑏 ⊆ { 0 } ) ) )
70 raleq ⊢ ( 𝑎 = 𝐵 → ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } ) )
71 raleq ⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } ) )
72 71 ralbidv ⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } ) )
73 70 72 sylan9bb ⊢ ( ( 𝑎 = 𝐵 ∧ 𝑏 = 𝐵 ) → ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } ) )
74 73 imbi1d ⊢ ( ( 𝑎 = 𝐵 ∧ 𝑏 = 𝐵 ) → ( ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } → ( 𝑎 ⊆ { 0 } ∨ 𝑏 ⊆ { 0 } ) ) ↔ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } → ( 𝑎 ⊆ { 0 } ∨ 𝑏 ⊆ { 0 } ) ) ) )
75 69 74 syl5ibrcom ⊢ ( 𝑅 ∈ NzRing → ( ( 𝑎 = 𝐵 ∧ 𝑏 = 𝐵 ) → ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } → ( 𝑎 ⊆ { 0 } ∨ 𝑏 ⊆ { 0 } ) ) ) )
76 37 41 43 75 ccased ⊢ ( 𝑅 ∈ NzRing → ( ( ( 𝑎 = { 0 } ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = { 0 } ∨ 𝑏 = 𝐵 ) ) → ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } → ( 𝑎 ⊆ { 0 } ∨ 𝑏 ⊆ { 0 } ) ) ) )
77 76 adantr ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) → ( ( ( 𝑎 = { 0 } ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = { 0 } ∨ 𝑏 = 𝐵 ) ) → ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } → ( 𝑎 ⊆ { 0 } ∨ 𝑏 ⊆ { 0 } ) ) ) )
78 33 77 sylbid ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) → ( ( 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ) → ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } → ( 𝑎 ⊆ { 0 } ∨ 𝑏 ⊆ { 0 } ) ) ) )
79 78 ralrimivv ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) → ∀ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } → ( 𝑎 ⊆ { 0 } ∨ 𝑏 ⊆ { 0 } ) ) )
80 1 51 isprmidl ⊢ ( 𝑅 ∈ Ring → ( { 0 } ∈ ( PrmIdeal ‘ 𝑅 ) ↔ ( { 0 } ∈ ( LIdeal ‘ 𝑅 ) ∧ { 0 } ≠ 𝐵 ∧ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } → ( 𝑎 ⊆ { 0 } ∨ 𝑏 ⊆ { 0 } ) ) ) ) )
81 4 80 syl ⊢ ( 𝑅 ∈ NzRing → ( { 0 } ∈ ( PrmIdeal ‘ 𝑅 ) ↔ ( { 0 } ∈ ( LIdeal ‘ 𝑅 ) ∧ { 0 } ≠ 𝐵 ∧ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } → ( 𝑎 ⊆ { 0 } ∨ 𝑏 ⊆ { 0 } ) ) ) ) )
82 81 adantr ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) → ( { 0 } ∈ ( PrmIdeal ‘ 𝑅 ) ↔ ( { 0 } ∈ ( LIdeal ‘ 𝑅 ) ∧ { 0 } ≠ 𝐵 ∧ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ { 0 } → ( 𝑎 ⊆ { 0 } ∨ 𝑏 ⊆ { 0 } ) ) ) ) )
83 9 12 79 82 mpbir3and ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) → { 0 } ∈ ( PrmIdeal ‘ 𝑅 ) )
84 eqid ⊢ ( PrmIdeal ‘ 𝑅 ) = ( PrmIdeal ‘ 𝑅 )
85 2 84 isprmrng ⊢ ( 𝑅 ∈ PrmRing ↔ ( 𝑅 ∈ Ring ∧ { 0 } ∈ ( PrmIdeal ‘ 𝑅 ) ) )
86 5 83 85 sylanbrc ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) → 𝑅 ∈ PrmRing )