Metamath Proof Explorer

Theorem ispridl

Description: The predicate "is a prime ideal". (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses pridlval.1 
|- G = ( 1st ` R )
pridlval.2 
|- H = ( 2nd ` R )
pridlval.3 
|- X = ran G
Assertion ispridl 
|- ( R e. RingOps -> ( P e. ( PrIdl ` R ) <-> ( P e. ( Idl ` R ) /\ P =/= X /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pridlval.1 
 |-  G = ( 1st ` R )
2 pridlval.2 
 |-  H = ( 2nd ` R )
3 pridlval.3 
 |-  X = ran G
4 1 2 3 pridlval 
 |-  ( R e. RingOps -> ( PrIdl ` R ) = { i e. ( Idl ` R ) | ( i =/= X /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } )
5 4 eleq2d 
 |-  ( R e. RingOps -> ( P e. ( PrIdl ` R ) <-> P e. { i e. ( Idl ` R ) | ( i =/= X /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } ) )
6 neeq1 
 |-  ( i = P -> ( i =/= X <-> P =/= X ) )
7 eleq2 
 |-  ( i = P -> ( ( x H y ) e. i <-> ( x H y ) e. P ) )
8 7 2ralbidv 
 |-  ( i = P -> ( A. x e. a A. y e. b ( x H y ) e. i <-> A. x e. a A. y e. b ( x H y ) e. P ) )
9 sseq2 
 |-  ( i = P -> ( a C_ i <-> a C_ P ) )
10 sseq2 
 |-  ( i = P -> ( b C_ i <-> b C_ P ) )
11 9 10 orbi12d 
 |-  ( i = P -> ( ( a C_ i \/ b C_ i ) <-> ( a C_ P \/ b C_ P ) ) )
12 8 11 imbi12d 
 |-  ( i = P -> ( ( A. x e. a A. y e. b ( x H y ) e. i -> ( a C_ i \/ b C_ i ) ) <-> ( A. x e. a A. y e. b ( x H y ) e. P -> ( a C_ P \/ b C_ P ) ) ) )
13 12 2ralbidv 
 |-  ( i = P -> ( A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. i -> ( a C_ i \/ b C_ i ) ) <-> A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. P -> ( a C_ P \/ b C_ P ) ) ) )
14 6 13 anbi12d 
 |-  ( i = P -> ( ( i =/= X /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. i -> ( a C_ i \/ b C_ i ) ) ) <-> ( P =/= X /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) )
15 14 elrab 
 |-  ( P e. { i e. ( Idl ` R ) | ( i =/= X /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } <-> ( P e. ( Idl ` R ) /\ ( P =/= X /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) )
16 3anass 
 |-  ( ( P e. ( Idl ` R ) /\ P =/= X /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. P -> ( a C_ P \/ b C_ P ) ) ) <-> ( P e. ( Idl ` R ) /\ ( P =/= X /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) )
17 15 16 bitr4i 
 |-  ( P e. { i e. ( Idl ` R ) | ( i =/= X /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } <-> ( P e. ( Idl ` R ) /\ P =/= X /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. P -> ( a C_ P \/ b C_ P ) ) ) )
18 5 17 bitrdi 
 |-  ( R e. RingOps -> ( P e. ( PrIdl ` R ) <-> ( P e. ( Idl ` R ) /\ P =/= X /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x H y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) )