This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
smprngpr.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
smprngpr.3 ⊢ 𝑋 = ran 𝐺
smprngpr.4 ⊢ 𝑍 = ( GId ‘ 𝐺 )
smprngpr.5 ⊢ 𝑈 = ( GId ‘ 𝐻 )
Assertion smprngopr ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ ( Idl ‘ 𝑅 ) = { { 𝑍 } , 𝑋 } ) → 𝑅 ∈ PrRing )

Proof

Step Hyp Ref Expression
1 smprngpr.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 smprngpr.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 smprngpr.3 ⊢ 𝑋 = ran 𝐺
4 smprngpr.4 ⊢ 𝑍 = ( GId ‘ 𝐺 )
5 smprngpr.5 ⊢ 𝑈 = ( GId ‘ 𝐻 )
6 simp1 ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ ( Idl ‘ 𝑅 ) = { { 𝑍 } , 𝑋 } ) → 𝑅 ∈ RingOps )
7 1 4 0idl ⊢ ( 𝑅 ∈ RingOps → { 𝑍 } ∈ ( Idl ‘ 𝑅 ) )
8 7 3ad2ant1 ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ ( Idl ‘ 𝑅 ) = { { 𝑍 } , 𝑋 } ) → { 𝑍 } ∈ ( Idl ‘ 𝑅 ) )
9 1 2 3 4 5 0rngo ⊢ ( 𝑅 ∈ RingOps → ( 𝑍 = 𝑈 ↔ 𝑋 = { 𝑍 } ) )
10 eqcom ⊢ ( 𝑈 = 𝑍 ↔ 𝑍 = 𝑈 )
11 eqcom ⊢ ( { 𝑍 } = 𝑋 ↔ 𝑋 = { 𝑍 } )
12 9 10 11 3bitr4g ⊢ ( 𝑅 ∈ RingOps → ( 𝑈 = 𝑍 ↔ { 𝑍 } = 𝑋 ) )
13 12 necon3bid ⊢ ( 𝑅 ∈ RingOps → ( 𝑈 ≠ 𝑍 ↔ { 𝑍 } ≠ 𝑋 ) )
14 13 biimpa ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ) → { 𝑍 } ≠ 𝑋 )
15 14 3adant3 ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ ( Idl ‘ 𝑅 ) = { { 𝑍 } , 𝑋 } ) → { 𝑍 } ≠ 𝑋 )
16 df-pr ⊢ { { 𝑍 } , 𝑋 } = ( { { 𝑍 } } ∪ { 𝑋 } )
17 16 eqeq2i ⊢ ( ( Idl ‘ 𝑅 ) = { { 𝑍 } , 𝑋 } ↔ ( Idl ‘ 𝑅 ) = ( { { 𝑍 } } ∪ { 𝑋 } ) )
18 eleq2 ⊢ ( ( Idl ‘ 𝑅 ) = ( { { 𝑍 } } ∪ { 𝑋 } ) → ( 𝑖 ∈ ( Idl ‘ 𝑅 ) ↔ 𝑖 ∈ ( { { 𝑍 } } ∪ { 𝑋 } ) ) )
19 eleq2 ⊢ ( ( Idl ‘ 𝑅 ) = ( { { 𝑍 } } ∪ { 𝑋 } ) → ( 𝑗 ∈ ( Idl ‘ 𝑅 ) ↔ 𝑗 ∈ ( { { 𝑍 } } ∪ { 𝑋 } ) ) )
20 18 19 anbi12d ⊢ ( ( Idl ‘ 𝑅 ) = ( { { 𝑍 } } ∪ { 𝑋 } ) → ( ( 𝑖 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑗 ∈ ( Idl ‘ 𝑅 ) ) ↔ ( 𝑖 ∈ ( { { 𝑍 } } ∪ { 𝑋 } ) ∧ 𝑗 ∈ ( { { 𝑍 } } ∪ { 𝑋 } ) ) ) )
21 elun ⊢ ( 𝑖 ∈ ( { { 𝑍 } } ∪ { 𝑋 } ) ↔ ( 𝑖 ∈ { { 𝑍 } } ∨ 𝑖 ∈ { 𝑋 } ) )
22 velsn ⊢ ( 𝑖 ∈ { { 𝑍 } } ↔ 𝑖 = { 𝑍 } )
23 velsn ⊢ ( 𝑖 ∈ { 𝑋 } ↔ 𝑖 = 𝑋 )
24 22 23 orbi12i ⊢ ( ( 𝑖 ∈ { { 𝑍 } } ∨ 𝑖 ∈ { 𝑋 } ) ↔ ( 𝑖 = { 𝑍 } ∨ 𝑖 = 𝑋 ) )
25 21 24 bitri ⊢ ( 𝑖 ∈ ( { { 𝑍 } } ∪ { 𝑋 } ) ↔ ( 𝑖 = { 𝑍 } ∨ 𝑖 = 𝑋 ) )
26 elun ⊢ ( 𝑗 ∈ ( { { 𝑍 } } ∪ { 𝑋 } ) ↔ ( 𝑗 ∈ { { 𝑍 } } ∨ 𝑗 ∈ { 𝑋 } ) )
27 velsn ⊢ ( 𝑗 ∈ { { 𝑍 } } ↔ 𝑗 = { 𝑍 } )
28 velsn ⊢ ( 𝑗 ∈ { 𝑋 } ↔ 𝑗 = 𝑋 )
29 27 28 orbi12i ⊢ ( ( 𝑗 ∈ { { 𝑍 } } ∨ 𝑗 ∈ { 𝑋 } ) ↔ ( 𝑗 = { 𝑍 } ∨ 𝑗 = 𝑋 ) )
30 26 29 bitri ⊢ ( 𝑗 ∈ ( { { 𝑍 } } ∪ { 𝑋 } ) ↔ ( 𝑗 = { 𝑍 } ∨ 𝑗 = 𝑋 ) )
31 25 30 anbi12i ⊢ ( ( 𝑖 ∈ ( { { 𝑍 } } ∪ { 𝑋 } ) ∧ 𝑗 ∈ ( { { 𝑍 } } ∪ { 𝑋 } ) ) ↔ ( ( 𝑖 = { 𝑍 } ∨ 𝑖 = 𝑋 ) ∧ ( 𝑗 = { 𝑍 } ∨ 𝑗 = 𝑋 ) ) )
32 20 31 bitrdi ⊢ ( ( Idl ‘ 𝑅 ) = ( { { 𝑍 } } ∪ { 𝑋 } ) → ( ( 𝑖 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑗 ∈ ( Idl ‘ 𝑅 ) ) ↔ ( ( 𝑖 = { 𝑍 } ∨ 𝑖 = 𝑋 ) ∧ ( 𝑗 = { 𝑍 } ∨ 𝑗 = 𝑋 ) ) ) )
33 17 32 sylbi ⊢ ( ( Idl ‘ 𝑅 ) = { { 𝑍 } , 𝑋 } → ( ( 𝑖 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑗 ∈ ( Idl ‘ 𝑅 ) ) ↔ ( ( 𝑖 = { 𝑍 } ∨ 𝑖 = 𝑋 ) ∧ ( 𝑗 = { 𝑍 } ∨ 𝑗 = 𝑋 ) ) ) )
34 33 3ad2ant3 ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ ( Idl ‘ 𝑅 ) = { { 𝑍 } , 𝑋 } ) → ( ( 𝑖 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑗 ∈ ( Idl ‘ 𝑅 ) ) ↔ ( ( 𝑖 = { 𝑍 } ∨ 𝑖 = 𝑋 ) ∧ ( 𝑗 = { 𝑍 } ∨ 𝑗 = 𝑋 ) ) ) )
35 eqimss ⊢ ( 𝑖 = { 𝑍 } → 𝑖 ⊆ { 𝑍 } )
36 35 orcd ⊢ ( 𝑖 = { 𝑍 } → ( 𝑖 ⊆ { 𝑍 } ∨ 𝑗 ⊆ { 𝑍 } ) )
37 36 adantr ⊢ ( ( 𝑖 = { 𝑍 } ∧ 𝑗 = { 𝑍 } ) → ( 𝑖 ⊆ { 𝑍 } ∨ 𝑗 ⊆ { 𝑍 } ) )
38 37 a1d ⊢ ( ( 𝑖 = { 𝑍 } ∧ 𝑗 = { 𝑍 } ) → ( ∀ 𝑥 ∈ 𝑖 ∀ 𝑦 ∈ 𝑗 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } → ( 𝑖 ⊆ { 𝑍 } ∨ 𝑗 ⊆ { 𝑍 } ) ) )
39 38 a1i ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ) → ( ( 𝑖 = { 𝑍 } ∧ 𝑗 = { 𝑍 } ) → ( ∀ 𝑥 ∈ 𝑖 ∀ 𝑦 ∈ 𝑗 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } → ( 𝑖 ⊆ { 𝑍 } ∨ 𝑗 ⊆ { 𝑍 } ) ) ) )
40 eqimss ⊢ ( 𝑗 = { 𝑍 } → 𝑗 ⊆ { 𝑍 } )
41 40 olcd ⊢ ( 𝑗 = { 𝑍 } → ( 𝑖 ⊆ { 𝑍 } ∨ 𝑗 ⊆ { 𝑍 } ) )
42 41 adantl ⊢ ( ( 𝑖 = 𝑋 ∧ 𝑗 = { 𝑍 } ) → ( 𝑖 ⊆ { 𝑍 } ∨ 𝑗 ⊆ { 𝑍 } ) )
43 42 a1d ⊢ ( ( 𝑖 = 𝑋 ∧ 𝑗 = { 𝑍 } ) → ( ∀ 𝑥 ∈ 𝑖 ∀ 𝑦 ∈ 𝑗 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } → ( 𝑖 ⊆ { 𝑍 } ∨ 𝑗 ⊆ { 𝑍 } ) ) )
44 43 a1i ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ) → ( ( 𝑖 = 𝑋 ∧ 𝑗 = { 𝑍 } ) → ( ∀ 𝑥 ∈ 𝑖 ∀ 𝑦 ∈ 𝑗 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } → ( 𝑖 ⊆ { 𝑍 } ∨ 𝑗 ⊆ { 𝑍 } ) ) ) )
45 36 adantr ⊢ ( ( 𝑖 = { 𝑍 } ∧ 𝑗 = 𝑋 ) → ( 𝑖 ⊆ { 𝑍 } ∨ 𝑗 ⊆ { 𝑍 } ) )
46 45 a1d ⊢ ( ( 𝑖 = { 𝑍 } ∧ 𝑗 = 𝑋 ) → ( ∀ 𝑥 ∈ 𝑖 ∀ 𝑦 ∈ 𝑗 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } → ( 𝑖 ⊆ { 𝑍 } ∨ 𝑗 ⊆ { 𝑍 } ) ) )
47 46 a1i ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ) → ( ( 𝑖 = { 𝑍 } ∧ 𝑗 = 𝑋 ) → ( ∀ 𝑥 ∈ 𝑖 ∀ 𝑦 ∈ 𝑗 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } → ( 𝑖 ⊆ { 𝑍 } ∨ 𝑗 ⊆ { 𝑍 } ) ) ) )
48 1 rneqi ⊢ ran 𝐺 = ran ( 1st ‘ 𝑅 )
49 3 48 eqtri ⊢ 𝑋 = ran ( 1st ‘ 𝑅 )
50 49 2 5 rngo1cl ⊢ ( 𝑅 ∈ RingOps → 𝑈 ∈ 𝑋 )
51 50 adantr ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ) → 𝑈 ∈ 𝑋 )
52 2 49 5 rngolidm ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑈 ∈ 𝑋 ) → ( 𝑈 𝐻 𝑈 ) = 𝑈 )
53 50 52 mpdan ⊢ ( 𝑅 ∈ RingOps → ( 𝑈 𝐻 𝑈 ) = 𝑈 )
54 53 eleq1d ⊢ ( 𝑅 ∈ RingOps → ( ( 𝑈 𝐻 𝑈 ) ∈ { 𝑍 } ↔ 𝑈 ∈ { 𝑍 } ) )
55 5 fvexi ⊢ 𝑈 ∈ V
56 55 elsn ⊢ ( 𝑈 ∈ { 𝑍 } ↔ 𝑈 = 𝑍 )
57 54 56 bitrdi ⊢ ( 𝑅 ∈ RingOps → ( ( 𝑈 𝐻 𝑈 ) ∈ { 𝑍 } ↔ 𝑈 = 𝑍 ) )
58 57 necon3bbid ⊢ ( 𝑅 ∈ RingOps → ( ¬ ( 𝑈 𝐻 𝑈 ) ∈ { 𝑍 } ↔ 𝑈 ≠ 𝑍 ) )
59 58 biimpar ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ) → ¬ ( 𝑈 𝐻 𝑈 ) ∈ { 𝑍 } )
60 oveq1 ⊢ ( 𝑥 = 𝑈 → ( 𝑥 𝐻 𝑦 ) = ( 𝑈 𝐻 𝑦 ) )
61 60 eleq1d ⊢ ( 𝑥 = 𝑈 → ( ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } ↔ ( 𝑈 𝐻 𝑦 ) ∈ { 𝑍 } ) )
62 61 notbid ⊢ ( 𝑥 = 𝑈 → ( ¬ ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } ↔ ¬ ( 𝑈 𝐻 𝑦 ) ∈ { 𝑍 } ) )
63 oveq2 ⊢ ( 𝑦 = 𝑈 → ( 𝑈 𝐻 𝑦 ) = ( 𝑈 𝐻 𝑈 ) )
64 63 eleq1d ⊢ ( 𝑦 = 𝑈 → ( ( 𝑈 𝐻 𝑦 ) ∈ { 𝑍 } ↔ ( 𝑈 𝐻 𝑈 ) ∈ { 𝑍 } ) )
65 64 notbid ⊢ ( 𝑦 = 𝑈 → ( ¬ ( 𝑈 𝐻 𝑦 ) ∈ { 𝑍 } ↔ ¬ ( 𝑈 𝐻 𝑈 ) ∈ { 𝑍 } ) )
66 62 65 rspc2ev ⊢ ( ( 𝑈 ∈ 𝑋 ∧ 𝑈 ∈ 𝑋 ∧ ¬ ( 𝑈 𝐻 𝑈 ) ∈ { 𝑍 } ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ¬ ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } )
67 51 51 59 66 syl3anc ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ¬ ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } )
68 rexnal2 ⊢ ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ¬ ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } ↔ ¬ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } )
69 67 68 sylib ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ) → ¬ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } )
70 69 pm2.21d ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } → ( 𝑖 ⊆ { 𝑍 } ∨ 𝑗 ⊆ { 𝑍 } ) ) )
71 raleq ⊢ ( 𝑖 = 𝑋 → ( ∀ 𝑥 ∈ 𝑖 ∀ 𝑦 ∈ 𝑗 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑗 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } ) )
72 raleq ⊢ ( 𝑗 = 𝑋 → ( ∀ 𝑦 ∈ 𝑗 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } ↔ ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } ) )
73 72 ralbidv ⊢ ( 𝑗 = 𝑋 → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑗 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } ) )
74 71 73 sylan9bb ⊢ ( ( 𝑖 = 𝑋 ∧ 𝑗 = 𝑋 ) → ( ∀ 𝑥 ∈ 𝑖 ∀ 𝑦 ∈ 𝑗 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } ) )
75 74 imbi1d ⊢ ( ( 𝑖 = 𝑋 ∧ 𝑗 = 𝑋 ) → ( ( ∀ 𝑥 ∈ 𝑖 ∀ 𝑦 ∈ 𝑗 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } → ( 𝑖 ⊆ { 𝑍 } ∨ 𝑗 ⊆ { 𝑍 } ) ) ↔ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } → ( 𝑖 ⊆ { 𝑍 } ∨ 𝑗 ⊆ { 𝑍 } ) ) ) )
76 70 75 syl5ibrcom ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ) → ( ( 𝑖 = 𝑋 ∧ 𝑗 = 𝑋 ) → ( ∀ 𝑥 ∈ 𝑖 ∀ 𝑦 ∈ 𝑗 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } → ( 𝑖 ⊆ { 𝑍 } ∨ 𝑗 ⊆ { 𝑍 } ) ) ) )
77 39 44 47 76 ccased ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ) → ( ( ( 𝑖 = { 𝑍 } ∨ 𝑖 = 𝑋 ) ∧ ( 𝑗 = { 𝑍 } ∨ 𝑗 = 𝑋 ) ) → ( ∀ 𝑥 ∈ 𝑖 ∀ 𝑦 ∈ 𝑗 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } → ( 𝑖 ⊆ { 𝑍 } ∨ 𝑗 ⊆ { 𝑍 } ) ) ) )
78 77 3adant3 ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ ( Idl ‘ 𝑅 ) = { { 𝑍 } , 𝑋 } ) → ( ( ( 𝑖 = { 𝑍 } ∨ 𝑖 = 𝑋 ) ∧ ( 𝑗 = { 𝑍 } ∨ 𝑗 = 𝑋 ) ) → ( ∀ 𝑥 ∈ 𝑖 ∀ 𝑦 ∈ 𝑗 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } → ( 𝑖 ⊆ { 𝑍 } ∨ 𝑗 ⊆ { 𝑍 } ) ) ) )
79 34 78 sylbid ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ ( Idl ‘ 𝑅 ) = { { 𝑍 } , 𝑋 } ) → ( ( 𝑖 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑗 ∈ ( Idl ‘ 𝑅 ) ) → ( ∀ 𝑥 ∈ 𝑖 ∀ 𝑦 ∈ 𝑗 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } → ( 𝑖 ⊆ { 𝑍 } ∨ 𝑗 ⊆ { 𝑍 } ) ) ) )
80 79 ralrimivv ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ ( Idl ‘ 𝑅 ) = { { 𝑍 } , 𝑋 } ) → ∀ 𝑖 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑖 ∀ 𝑦 ∈ 𝑗 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } → ( 𝑖 ⊆ { 𝑍 } ∨ 𝑗 ⊆ { 𝑍 } ) ) )
81 1 2 3 ispridl ⊢ ( 𝑅 ∈ RingOps → ( { 𝑍 } ∈ ( PrIdl ‘ 𝑅 ) ↔ ( { 𝑍 } ∈ ( Idl ‘ 𝑅 ) ∧ { 𝑍 } ≠ 𝑋 ∧ ∀ 𝑖 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑖 ∀ 𝑦 ∈ 𝑗 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } → ( 𝑖 ⊆ { 𝑍 } ∨ 𝑗 ⊆ { 𝑍 } ) ) ) ) )
82 81 3ad2ant1 ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ ( Idl ‘ 𝑅 ) = { { 𝑍 } , 𝑋 } ) → ( { 𝑍 } ∈ ( PrIdl ‘ 𝑅 ) ↔ ( { 𝑍 } ∈ ( Idl ‘ 𝑅 ) ∧ { 𝑍 } ≠ 𝑋 ∧ ∀ 𝑖 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑗 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑖 ∀ 𝑦 ∈ 𝑗 ( 𝑥 𝐻 𝑦 ) ∈ { 𝑍 } → ( 𝑖 ⊆ { 𝑍 } ∨ 𝑗 ⊆ { 𝑍 } ) ) ) ) )
83 8 15 80 82 mpbir3and ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ ( Idl ‘ 𝑅 ) = { { 𝑍 } , 𝑋 } ) → { 𝑍 } ∈ ( PrIdl ‘ 𝑅 ) )
84 1 4 isprrngo ⊢ ( 𝑅 ∈ PrRing ↔ ( 𝑅 ∈ RingOps ∧ { 𝑍 } ∈ ( PrIdl ‘ 𝑅 ) ) )
85 6 83 84 sylanbrc ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ ( Idl ‘ 𝑅 ) = { { 𝑍 } , 𝑋 } ) → 𝑅 ∈ PrRing )