Metamath Proof Explorer

Theorem isprmidl

Description: The predicate "is a prime ideal". (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Thierry Arnoux, 12-Jan-2024)

Ref Expression
Hypotheses prmidlval.1 
|- B = ( Base ` R )
prmidlval.2 
|- .x. = ( .r ` R )
Assertion isprmidl 
|- ( R e. Ring -> ( P e. ( PrmIdeal ` R ) <-> ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) )

Proof

Step Hyp Ref Expression
1 prmidlval.1 
 |-  B = ( Base ` R )
2 prmidlval.2 
 |-  .x. = ( .r ` R )
3 1 2 prmidlval 
 |-  ( R e. Ring -> ( PrmIdeal ` R ) = { i e. ( LIdeal ` R ) | ( i =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } )
4 3 eleq2d 
 |-  ( R e. Ring -> ( P e. ( PrmIdeal ` R ) <-> P e. { i e. ( LIdeal ` R ) | ( i =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } ) )
5 neeq1 
 |-  ( i = P -> ( i =/= B <-> P =/= B ) )
6 eleq2 
 |-  ( i = P -> ( ( x .x. y ) e. i <-> ( x .x. y ) e. P ) )
7 6 2ralbidv 
 |-  ( i = P -> ( A. x e. a A. y e. b ( x .x. y ) e. i <-> A. x e. a A. y e. b ( x .x. y ) e. P ) )
8 sseq2 
 |-  ( i = P -> ( a C_ i <-> a C_ P ) )
9 sseq2 
 |-  ( i = P -> ( b C_ i <-> b C_ P ) )
10 8 9 orbi12d 
 |-  ( i = P -> ( ( a C_ i \/ b C_ i ) <-> ( a C_ P \/ b C_ P ) ) )
11 7 10 imbi12d 
 |-  ( i = P -> ( ( A. x e. a A. y e. b ( x .x. y ) e. i -> ( a C_ i \/ b C_ i ) ) <-> ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) )
12 11 2ralbidv 
 |-  ( i = P -> ( A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. i -> ( a C_ i \/ b C_ i ) ) <-> A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) )
13 5 12 anbi12d 
 |-  ( i = P -> ( ( i =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. i -> ( a C_ i \/ b C_ i ) ) ) <-> ( P =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) )
14 13 elrab 
 |-  ( P e. { i e. ( LIdeal ` R ) | ( i =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. i -> ( a C_ i \/ b C_ i ) ) ) } <-> ( P e. ( LIdeal ` R ) /\ ( P =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) )
15 4 14 bitrdi 
 |-  ( R e. Ring -> ( P e. ( PrmIdeal ` R ) <-> ( P e. ( LIdeal ` R ) /\ ( P =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) ) )
16 3anass 
 |-  ( ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) <-> ( P e. ( LIdeal ` R ) /\ ( P =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) )
17 15 16 bitr4di 
 |-  ( R e. Ring -> ( P e. ( PrmIdeal ` R ) <-> ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) )