Metamath Proof Explorer

Theorem ispridlc

Description: The predicate "is a prime ideal". Alternate definition for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010)

Ref Expression
Hypotheses ispridlc.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
ispridlc.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
ispridlc.3 ⊢ 𝑋 = ran 𝐺
Assertion ispridlc ( 𝑅 ∈ CRingOps → ( 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ↔ ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ispridlc.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 ispridlc.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 ispridlc.3 ⊢ 𝑋 = ran 𝐺
4 crngorngo ⊢ ( 𝑅 ∈ CRingOps → 𝑅 ∈ RingOps )
5 1 2 3 ispridl ⊢ ( 𝑅 ∈ RingOps → ( 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ↔ ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑟 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑠 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) ) ) )
6 4 5 syl ⊢ ( 𝑅 ∈ CRingOps → ( 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ↔ ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑟 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑠 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) ) ) )
7 snssi ⊢ ( 𝑎 ∈ 𝑋 → { 𝑎 } ⊆ 𝑋 )
8 1 3 igenidl ⊢ ( ( 𝑅 ∈ RingOps ∧ { 𝑎 } ⊆ 𝑋 ) → ( 𝑅 IdlGen { 𝑎 } ) ∈ ( Idl ‘ 𝑅 ) )
9 4 7 8 syl2an ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋 ) → ( 𝑅 IdlGen { 𝑎 } ) ∈ ( Idl ‘ 𝑅 ) )
10 9 adantrr ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑅 IdlGen { 𝑎 } ) ∈ ( Idl ‘ 𝑅 ) )
11 snssi ⊢ ( 𝑏 ∈ 𝑋 → { 𝑏 } ⊆ 𝑋 )
12 1 3 igenidl ⊢ ( ( 𝑅 ∈ RingOps ∧ { 𝑏 } ⊆ 𝑋 ) → ( 𝑅 IdlGen { 𝑏 } ) ∈ ( Idl ‘ 𝑅 ) )
13 4 11 12 syl2an ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋 ) → ( 𝑅 IdlGen { 𝑏 } ) ∈ ( Idl ‘ 𝑅 ) )
14 13 adantrl ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑅 IdlGen { 𝑏 } ) ∈ ( Idl ‘ 𝑅 ) )
15 raleq ⊢ ( 𝑟 = ( 𝑅 IdlGen { 𝑎 } ) → ( ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ↔ ∀ 𝑥 ∈ ( 𝑅 IdlGen { 𝑎 } ) ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ) )
16 sseq1 ⊢ ( 𝑟 = ( 𝑅 IdlGen { 𝑎 } ) → ( 𝑟 ⊆ 𝑃 ↔ ( 𝑅 IdlGen { 𝑎 } ) ⊆ 𝑃 ) )
17 16 orbi1d ⊢ ( 𝑟 = ( 𝑅 IdlGen { 𝑎 } ) → ( ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ↔ ( ( 𝑅 IdlGen { 𝑎 } ) ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) )
18 15 17 imbi12d ⊢ ( 𝑟 = ( 𝑅 IdlGen { 𝑎 } ) → ( ( ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) ↔ ( ∀ 𝑥 ∈ ( 𝑅 IdlGen { 𝑎 } ) ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( ( 𝑅 IdlGen { 𝑎 } ) ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) ) )
19 raleq ⊢ ( 𝑠 = ( 𝑅 IdlGen { 𝑏 } ) → ( ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ↔ ∀ 𝑦 ∈ ( 𝑅 IdlGen { 𝑏 } ) ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ) )
20 19 ralbidv ⊢ ( 𝑠 = ( 𝑅 IdlGen { 𝑏 } ) → ( ∀ 𝑥 ∈ ( 𝑅 IdlGen { 𝑎 } ) ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ↔ ∀ 𝑥 ∈ ( 𝑅 IdlGen { 𝑎 } ) ∀ 𝑦 ∈ ( 𝑅 IdlGen { 𝑏 } ) ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ) )
21 sseq1 ⊢ ( 𝑠 = ( 𝑅 IdlGen { 𝑏 } ) → ( 𝑠 ⊆ 𝑃 ↔ ( 𝑅 IdlGen { 𝑏 } ) ⊆ 𝑃 ) )
22 21 orbi2d ⊢ ( 𝑠 = ( 𝑅 IdlGen { 𝑏 } ) → ( ( ( 𝑅 IdlGen { 𝑎 } ) ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ↔ ( ( 𝑅 IdlGen { 𝑎 } ) ⊆ 𝑃 ∨ ( 𝑅 IdlGen { 𝑏 } ) ⊆ 𝑃 ) ) )
23 20 22 imbi12d ⊢ ( 𝑠 = ( 𝑅 IdlGen { 𝑏 } ) → ( ( ∀ 𝑥 ∈ ( 𝑅 IdlGen { 𝑎 } ) ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( ( 𝑅 IdlGen { 𝑎 } ) ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) ↔ ( ∀ 𝑥 ∈ ( 𝑅 IdlGen { 𝑎 } ) ∀ 𝑦 ∈ ( 𝑅 IdlGen { 𝑏 } ) ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( ( 𝑅 IdlGen { 𝑎 } ) ⊆ 𝑃 ∨ ( 𝑅 IdlGen { 𝑏 } ) ⊆ 𝑃 ) ) ) )
24 18 23 rspc2v ⊢ ( ( ( 𝑅 IdlGen { 𝑎 } ) ∈ ( Idl ‘ 𝑅 ) ∧ ( 𝑅 IdlGen { 𝑏 } ) ∈ ( Idl ‘ 𝑅 ) ) → ( ∀ 𝑟 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑠 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) → ( ∀ 𝑥 ∈ ( 𝑅 IdlGen { 𝑎 } ) ∀ 𝑦 ∈ ( 𝑅 IdlGen { 𝑏 } ) ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( ( 𝑅 IdlGen { 𝑎 } ) ⊆ 𝑃 ∨ ( 𝑅 IdlGen { 𝑏 } ) ⊆ 𝑃 ) ) ) )
25 10 14 24 syl2anc ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ∀ 𝑟 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑠 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) → ( ∀ 𝑥 ∈ ( 𝑅 IdlGen { 𝑎 } ) ∀ 𝑦 ∈ ( 𝑅 IdlGen { 𝑏 } ) ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( ( 𝑅 IdlGen { 𝑎 } ) ⊆ 𝑃 ∨ ( 𝑅 IdlGen { 𝑏 } ) ⊆ 𝑃 ) ) ) )
26 25 adantlr ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ∀ 𝑟 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑠 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) → ( ∀ 𝑥 ∈ ( 𝑅 IdlGen { 𝑎 } ) ∀ 𝑦 ∈ ( 𝑅 IdlGen { 𝑏 } ) ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( ( 𝑅 IdlGen { 𝑎 } ) ⊆ 𝑃 ∨ ( 𝑅 IdlGen { 𝑏 } ) ⊆ 𝑃 ) ) ) )
27 1 2 3 prnc ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋 ) → ( 𝑅 IdlGen { 𝑎 } ) = { 𝑥 ∈ 𝑋 ∣ ∃ 𝑟 ∈ 𝑋 𝑥 = ( 𝑟 𝐻 𝑎 ) } )
28 df-rab ⊢ { 𝑥 ∈ 𝑋 ∣ ∃ 𝑟 ∈ 𝑋 𝑥 = ( 𝑟 𝐻 𝑎 ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝑋 ∧ ∃ 𝑟 ∈ 𝑋 𝑥 = ( 𝑟 𝐻 𝑎 ) ) }
29 27 28 eqtrdi ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋 ) → ( 𝑅 IdlGen { 𝑎 } ) = { 𝑥 ∣ ( 𝑥 ∈ 𝑋 ∧ ∃ 𝑟 ∈ 𝑋 𝑥 = ( 𝑟 𝐻 𝑎 ) ) } )
30 29 eqabrd ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋 ) → ( 𝑥 ∈ ( 𝑅 IdlGen { 𝑎 } ) ↔ ( 𝑥 ∈ 𝑋 ∧ ∃ 𝑟 ∈ 𝑋 𝑥 = ( 𝑟 𝐻 𝑎 ) ) ) )
31 30 adantrr ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑥 ∈ ( 𝑅 IdlGen { 𝑎 } ) ↔ ( 𝑥 ∈ 𝑋 ∧ ∃ 𝑟 ∈ 𝑋 𝑥 = ( 𝑟 𝐻 𝑎 ) ) ) )
32 1 2 3 prnc ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋 ) → ( 𝑅 IdlGen { 𝑏 } ) = { 𝑦 ∈ 𝑋 ∣ ∃ 𝑠 ∈ 𝑋 𝑦 = ( 𝑠 𝐻 𝑏 ) } )
33 df-rab ⊢ { 𝑦 ∈ 𝑋 ∣ ∃ 𝑠 ∈ 𝑋 𝑦 = ( 𝑠 𝐻 𝑏 ) } = { 𝑦 ∣ ( 𝑦 ∈ 𝑋 ∧ ∃ 𝑠 ∈ 𝑋 𝑦 = ( 𝑠 𝐻 𝑏 ) ) }
34 32 33 eqtrdi ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋 ) → ( 𝑅 IdlGen { 𝑏 } ) = { 𝑦 ∣ ( 𝑦 ∈ 𝑋 ∧ ∃ 𝑠 ∈ 𝑋 𝑦 = ( 𝑠 𝐻 𝑏 ) ) } )
35 34 eqabrd ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋 ) → ( 𝑦 ∈ ( 𝑅 IdlGen { 𝑏 } ) ↔ ( 𝑦 ∈ 𝑋 ∧ ∃ 𝑠 ∈ 𝑋 𝑦 = ( 𝑠 𝐻 𝑏 ) ) ) )
36 35 adantrl ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑦 ∈ ( 𝑅 IdlGen { 𝑏 } ) ↔ ( 𝑦 ∈ 𝑋 ∧ ∃ 𝑠 ∈ 𝑋 𝑦 = ( 𝑠 𝐻 𝑏 ) ) ) )
37 31 36 anbi12d ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( 𝑥 ∈ ( 𝑅 IdlGen { 𝑎 } ) ∧ 𝑦 ∈ ( 𝑅 IdlGen { 𝑏 } ) ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ ∃ 𝑟 ∈ 𝑋 𝑥 = ( 𝑟 𝐻 𝑎 ) ) ∧ ( 𝑦 ∈ 𝑋 ∧ ∃ 𝑠 ∈ 𝑋 𝑦 = ( 𝑠 𝐻 𝑏 ) ) ) ) )
38 37 adantlr ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( 𝑥 ∈ ( 𝑅 IdlGen { 𝑎 } ) ∧ 𝑦 ∈ ( 𝑅 IdlGen { 𝑏 } ) ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ ∃ 𝑟 ∈ 𝑋 𝑥 = ( 𝑟 𝐻 𝑎 ) ) ∧ ( 𝑦 ∈ 𝑋 ∧ ∃ 𝑠 ∈ 𝑋 𝑦 = ( 𝑠 𝐻 𝑏 ) ) ) ) )
39 38 adantr ⊢ ( ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 ) → ( ( 𝑥 ∈ ( 𝑅 IdlGen { 𝑎 } ) ∧ 𝑦 ∈ ( 𝑅 IdlGen { 𝑏 } ) ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ ∃ 𝑟 ∈ 𝑋 𝑥 = ( 𝑟 𝐻 𝑎 ) ) ∧ ( 𝑦 ∈ 𝑋 ∧ ∃ 𝑠 ∈ 𝑋 𝑦 = ( 𝑠 𝐻 𝑏 ) ) ) ) )
40 reeanv ⊢ ( ∃ 𝑟 ∈ 𝑋 ∃ 𝑠 ∈ 𝑋 ( 𝑥 = ( 𝑟 𝐻 𝑎 ) ∧ 𝑦 = ( 𝑠 𝐻 𝑏 ) ) ↔ ( ∃ 𝑟 ∈ 𝑋 𝑥 = ( 𝑟 𝐻 𝑎 ) ∧ ∃ 𝑠 ∈ 𝑋 𝑦 = ( 𝑠 𝐻 𝑏 ) ) )
41 40 anbi2i ⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ∃ 𝑟 ∈ 𝑋 ∃ 𝑠 ∈ 𝑋 ( 𝑥 = ( 𝑟 𝐻 𝑎 ) ∧ 𝑦 = ( 𝑠 𝐻 𝑏 ) ) ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( ∃ 𝑟 ∈ 𝑋 𝑥 = ( 𝑟 𝐻 𝑎 ) ∧ ∃ 𝑠 ∈ 𝑋 𝑦 = ( 𝑠 𝐻 𝑏 ) ) ) )
42 an4 ⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( ∃ 𝑟 ∈ 𝑋 𝑥 = ( 𝑟 𝐻 𝑎 ) ∧ ∃ 𝑠 ∈ 𝑋 𝑦 = ( 𝑠 𝐻 𝑏 ) ) ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ ∃ 𝑟 ∈ 𝑋 𝑥 = ( 𝑟 𝐻 𝑎 ) ) ∧ ( 𝑦 ∈ 𝑋 ∧ ∃ 𝑠 ∈ 𝑋 𝑦 = ( 𝑠 𝐻 𝑏 ) ) ) )
43 41 42 bitri ⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ∃ 𝑟 ∈ 𝑋 ∃ 𝑠 ∈ 𝑋 ( 𝑥 = ( 𝑟 𝐻 𝑎 ) ∧ 𝑦 = ( 𝑠 𝐻 𝑏 ) ) ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ ∃ 𝑟 ∈ 𝑋 𝑥 = ( 𝑟 𝐻 𝑎 ) ) ∧ ( 𝑦 ∈ 𝑋 ∧ ∃ 𝑠 ∈ 𝑋 𝑦 = ( 𝑠 𝐻 𝑏 ) ) ) )
44 1 2 3 crngm4 ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( 𝑟 𝐻 𝑠 ) 𝐻 ( 𝑎 𝐻 𝑏 ) ) = ( ( 𝑟 𝐻 𝑎 ) 𝐻 ( 𝑠 𝐻 𝑏 ) ) )
45 44 3com23 ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ) ) → ( ( 𝑟 𝐻 𝑠 ) 𝐻 ( 𝑎 𝐻 𝑏 ) ) = ( ( 𝑟 𝐻 𝑎 ) 𝐻 ( 𝑠 𝐻 𝑏 ) ) )
46 45 3expa ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ) ) → ( ( 𝑟 𝐻 𝑠 ) 𝐻 ( 𝑎 𝐻 𝑏 ) ) = ( ( 𝑟 𝐻 𝑎 ) 𝐻 ( 𝑠 𝐻 𝑏 ) ) )
47 46 adantllr ⊢ ( ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ) ) → ( ( 𝑟 𝐻 𝑠 ) 𝐻 ( 𝑎 𝐻 𝑏 ) ) = ( ( 𝑟 𝐻 𝑎 ) 𝐻 ( 𝑠 𝐻 𝑏 ) ) )
48 47 adantlr ⊢ ( ( ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ) ) → ( ( 𝑟 𝐻 𝑠 ) 𝐻 ( 𝑎 𝐻 𝑏 ) ) = ( ( 𝑟 𝐻 𝑎 ) 𝐻 ( 𝑠 𝐻 𝑏 ) ) )
49 1 2 3 rngocl ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑟 𝐻 𝑠 ) ∈ 𝑋 )
50 4 49 syl3an1 ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑟 𝐻 𝑠 ) ∈ 𝑋 )
51 50 3expb ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ) ) → ( 𝑟 𝐻 𝑠 ) ∈ 𝑋 )
52 51 adantlr ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ) ) → ( 𝑟 𝐻 𝑠 ) ∈ 𝑋 )
53 52 adantlr ⊢ ( ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ) ) → ( 𝑟 𝐻 𝑠 ) ∈ 𝑋 )
54 1 2 3 idllmulcl ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 ∧ ( 𝑟 𝐻 𝑠 ) ∈ 𝑋 ) ) → ( ( 𝑟 𝐻 𝑠 ) 𝐻 ( 𝑎 𝐻 𝑏 ) ) ∈ 𝑃 )
55 4 54 sylanl1 ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 ∧ ( 𝑟 𝐻 𝑠 ) ∈ 𝑋 ) ) → ( ( 𝑟 𝐻 𝑠 ) 𝐻 ( 𝑎 𝐻 𝑏 ) ) ∈ 𝑃 )
56 55 anassrs ⊢ ( ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 ) ∧ ( 𝑟 𝐻 𝑠 ) ∈ 𝑋 ) → ( ( 𝑟 𝐻 𝑠 ) 𝐻 ( 𝑎 𝐻 𝑏 ) ) ∈ 𝑃 )
57 53 56 syldan ⊢ ( ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ) ) → ( ( 𝑟 𝐻 𝑠 ) 𝐻 ( 𝑎 𝐻 𝑏 ) ) ∈ 𝑃 )
58 57 adantllr ⊢ ( ( ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ) ) → ( ( 𝑟 𝐻 𝑠 ) 𝐻 ( 𝑎 𝐻 𝑏 ) ) ∈ 𝑃 )
59 48 58 eqeltrrd ⊢ ( ( ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ) ) → ( ( 𝑟 𝐻 𝑎 ) 𝐻 ( 𝑠 𝐻 𝑏 ) ) ∈ 𝑃 )
60 oveq12 ⊢ ( ( 𝑥 = ( 𝑟 𝐻 𝑎 ) ∧ 𝑦 = ( 𝑠 𝐻 𝑏 ) ) → ( 𝑥 𝐻 𝑦 ) = ( ( 𝑟 𝐻 𝑎 ) 𝐻 ( 𝑠 𝐻 𝑏 ) ) )
61 60 eleq1d ⊢ ( ( 𝑥 = ( 𝑟 𝐻 𝑎 ) ∧ 𝑦 = ( 𝑠 𝐻 𝑏 ) ) → ( ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ↔ ( ( 𝑟 𝐻 𝑎 ) 𝐻 ( 𝑠 𝐻 𝑏 ) ) ∈ 𝑃 ) )
62 59 61 syl5ibrcom ⊢ ( ( ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ) ) → ( ( 𝑥 = ( 𝑟 𝐻 𝑎 ) ∧ 𝑦 = ( 𝑠 𝐻 𝑏 ) ) → ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ) )
63 62 rexlimdvva ⊢ ( ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 ) → ( ∃ 𝑟 ∈ 𝑋 ∃ 𝑠 ∈ 𝑋 ( 𝑥 = ( 𝑟 𝐻 𝑎 ) ∧ 𝑦 = ( 𝑠 𝐻 𝑏 ) ) → ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ) )
64 63 adantld ⊢ ( ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 ) → ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ∃ 𝑟 ∈ 𝑋 ∃ 𝑠 ∈ 𝑋 ( 𝑥 = ( 𝑟 𝐻 𝑎 ) ∧ 𝑦 = ( 𝑠 𝐻 𝑏 ) ) ) → ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ) )
65 43 64 biimtrrid ⊢ ( ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 ) → ( ( ( 𝑥 ∈ 𝑋 ∧ ∃ 𝑟 ∈ 𝑋 𝑥 = ( 𝑟 𝐻 𝑎 ) ) ∧ ( 𝑦 ∈ 𝑋 ∧ ∃ 𝑠 ∈ 𝑋 𝑦 = ( 𝑠 𝐻 𝑏 ) ) ) → ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ) )
66 39 65 sylbid ⊢ ( ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 ) → ( ( 𝑥 ∈ ( 𝑅 IdlGen { 𝑎 } ) ∧ 𝑦 ∈ ( 𝑅 IdlGen { 𝑏 } ) ) → ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ) )
67 66 ralrimivv ⊢ ( ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 ) → ∀ 𝑥 ∈ ( 𝑅 IdlGen { 𝑎 } ) ∀ 𝑦 ∈ ( 𝑅 IdlGen { 𝑏 } ) ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 )
68 67 ex ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ∀ 𝑥 ∈ ( 𝑅 IdlGen { 𝑎 } ) ∀ 𝑦 ∈ ( 𝑅 IdlGen { 𝑏 } ) ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 ) )
69 1 3 igenss ⊢ ( ( 𝑅 ∈ RingOps ∧ { 𝑎 } ⊆ 𝑋 ) → { 𝑎 } ⊆ ( 𝑅 IdlGen { 𝑎 } ) )
70 4 7 69 syl2an ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋 ) → { 𝑎 } ⊆ ( 𝑅 IdlGen { 𝑎 } ) )
71 vex ⊢ 𝑎 ∈ V
72 71 snss ⊢ ( 𝑎 ∈ ( 𝑅 IdlGen { 𝑎 } ) ↔ { 𝑎 } ⊆ ( 𝑅 IdlGen { 𝑎 } ) )
73 70 72 sylibr ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋 ) → 𝑎 ∈ ( 𝑅 IdlGen { 𝑎 } ) )
74 73 adantrr ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → 𝑎 ∈ ( 𝑅 IdlGen { 𝑎 } ) )
75 ssel ⊢ ( ( 𝑅 IdlGen { 𝑎 } ) ⊆ 𝑃 → ( 𝑎 ∈ ( 𝑅 IdlGen { 𝑎 } ) → 𝑎 ∈ 𝑃 ) )
76 74 75 syl5com ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( 𝑅 IdlGen { 𝑎 } ) ⊆ 𝑃 → 𝑎 ∈ 𝑃 ) )
77 1 3 igenss ⊢ ( ( 𝑅 ∈ RingOps ∧ { 𝑏 } ⊆ 𝑋 ) → { 𝑏 } ⊆ ( 𝑅 IdlGen { 𝑏 } ) )
78 4 11 77 syl2an ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋 ) → { 𝑏 } ⊆ ( 𝑅 IdlGen { 𝑏 } ) )
79 vex ⊢ 𝑏 ∈ V
80 79 snss ⊢ ( 𝑏 ∈ ( 𝑅 IdlGen { 𝑏 } ) ↔ { 𝑏 } ⊆ ( 𝑅 IdlGen { 𝑏 } ) )
81 78 80 sylibr ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋 ) → 𝑏 ∈ ( 𝑅 IdlGen { 𝑏 } ) )
82 81 adantrl ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → 𝑏 ∈ ( 𝑅 IdlGen { 𝑏 } ) )
83 ssel ⊢ ( ( 𝑅 IdlGen { 𝑏 } ) ⊆ 𝑃 → ( 𝑏 ∈ ( 𝑅 IdlGen { 𝑏 } ) → 𝑏 ∈ 𝑃 ) )
84 82 83 syl5com ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( 𝑅 IdlGen { 𝑏 } ) ⊆ 𝑃 → 𝑏 ∈ 𝑃 ) )
85 76 84 orim12d ⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( ( 𝑅 IdlGen { 𝑎 } ) ⊆ 𝑃 ∨ ( 𝑅 IdlGen { 𝑏 } ) ⊆ 𝑃 ) → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) )
86 85 adantlr ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( ( 𝑅 IdlGen { 𝑎 } ) ⊆ 𝑃 ∨ ( 𝑅 IdlGen { 𝑏 } ) ⊆ 𝑃 ) → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) )
87 68 86 imim12d ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( ∀ 𝑥 ∈ ( 𝑅 IdlGen { 𝑎 } ) ∀ 𝑦 ∈ ( 𝑅 IdlGen { 𝑏 } ) ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( ( 𝑅 IdlGen { 𝑎 } ) ⊆ 𝑃 ∨ ( 𝑅 IdlGen { 𝑏 } ) ⊆ 𝑃 ) ) → ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) )
88 26 87 syld ⊢ ( ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ∀ 𝑟 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑠 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) → ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) )
89 88 ralrimdvva ⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝑃 ∈ ( Idl ‘ 𝑅 ) ) → ( ∀ 𝑟 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑠 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) → ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) )
90 89 ex ⊢ ( 𝑅 ∈ CRingOps → ( 𝑃 ∈ ( Idl ‘ 𝑅 ) → ( ∀ 𝑟 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑠 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) → ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) ) )
91 90 adantrd ⊢ ( 𝑅 ∈ CRingOps → ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ) → ( ∀ 𝑟 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑠 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) → ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) ) )
92 91 imdistand ⊢ ( 𝑅 ∈ CRingOps → ( ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ) ∧ ∀ 𝑟 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑠 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) ) → ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ) ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) ) )
93 df-3an ⊢ ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑟 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑠 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) ) ↔ ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ) ∧ ∀ 𝑟 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑠 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) ) )
94 df-3an ⊢ ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) ↔ ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ) ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) )
95 92 93 94 3imtr4g ⊢ ( 𝑅 ∈ CRingOps → ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑟 ∈ ( Idl ‘ 𝑅 ) ∀ 𝑠 ∈ ( Idl ‘ 𝑅 ) ( ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐻 𝑦 ) ∈ 𝑃 → ( 𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃 ) ) ) → ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) ) )
96 6 95 sylbid ⊢ ( 𝑅 ∈ CRingOps → ( 𝑃 ∈ ( PrIdl ‘ 𝑅 ) → ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) ) )
97 1 2 3 ispridl2 ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) ) → 𝑃 ∈ ( PrIdl ‘ 𝑅 ) )
98 97 ex ⊢ ( 𝑅 ∈ RingOps → ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) → 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) )
99 4 98 syl ⊢ ( 𝑅 ∈ CRingOps → ( ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) → 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ) )
100 96 99 impbid ⊢ ( 𝑅 ∈ CRingOps → ( 𝑃 ∈ ( PrIdl ‘ 𝑅 ) ↔ ( 𝑃 ∈ ( Idl ‘ 𝑅 ) ∧ 𝑃 ≠ 𝑋 ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ( 𝑎 𝐻 𝑏 ) ∈ 𝑃 → ( 𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃 ) ) ) ) )