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

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 
|- G = ( 1st ` R )
ispridlc.2 
|- H = ( 2nd ` R )
ispridlc.3 
|- X = ran G
Assertion ispridlc 
|- ( R e. CRingOps -> ( P e. ( PrIdl ` R ) <-> ( P e. ( Idl ` R ) /\ P =/= X /\ A. a e. X A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) ) ) )

Proof

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