Metamath Proof Explorer

Theorem prmidl2

Description: A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc for the equivalence in the commutative case. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Thierry Arnoux, 12-Jan-2024)

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

Proof

Step Hyp Ref Expression
1 prmidlval.1 
 |-  B = ( Base ` R )
2 prmidlval.2 
 |-  .x. = ( .r ` R )
3 simpr 
 |-  ( ( ( ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ P =/= B ) /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) /\ ( a e. ( LIdeal ` R ) /\ b e. ( LIdeal ` R ) ) ) /\ A. x e. a A. y e. b ( x .x. y ) e. P ) -> A. x e. a A. y e. b ( x .x. y ) e. P )
4 simplrr 
 |-  ( ( ( ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ P =/= B ) /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) /\ ( a e. ( LIdeal ` R ) /\ b e. ( LIdeal ` R ) ) ) /\ A. x e. a A. y e. b ( x .x. y ) e. P ) -> b e. ( LIdeal ` R ) )
5 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
6 1 5 lidlss 
 |-  ( b e. ( LIdeal ` R ) -> b C_ B )
7 4 6 syl 
 |-  ( ( ( ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ P =/= B ) /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) /\ ( a e. ( LIdeal ` R ) /\ b e. ( LIdeal ` R ) ) ) /\ A. x e. a A. y e. b ( x .x. y ) e. P ) -> b C_ B )
8 simplrl 
 |-  ( ( ( ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ P =/= B ) /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) /\ ( a e. ( LIdeal ` R ) /\ b e. ( LIdeal ` R ) ) ) /\ A. x e. a A. y e. b ( x .x. y ) e. P ) -> a e. ( LIdeal ` R ) )
9 1 5 lidlss 
 |-  ( a e. ( LIdeal ` R ) -> a C_ B )
10 8 9 syl 
 |-  ( ( ( ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ P =/= B ) /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) /\ ( a e. ( LIdeal ` R ) /\ b e. ( LIdeal ` R ) ) ) /\ A. x e. a A. y e. b ( x .x. y ) e. P ) -> a C_ B )
11 simpllr 
 |-  ( ( ( ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ P =/= B ) /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) /\ ( a e. ( LIdeal ` R ) /\ b e. ( LIdeal ` R ) ) ) /\ A. x e. a A. y e. b ( x .x. y ) e. P ) -> A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) )
12 ssralv 
 |-  ( a C_ B -> ( A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) -> A. x e. a A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) )
13 10 11 12 sylc 
 |-  ( ( ( ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ P =/= B ) /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) /\ ( a e. ( LIdeal ` R ) /\ b e. ( LIdeal ` R ) ) ) /\ A. x e. a A. y e. b ( x .x. y ) e. P ) -> A. x e. a A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) )
14 ssralv 
 |-  ( b C_ B -> ( A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) -> A. y e. b ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) )
15 14 ralimdv 
 |-  ( b C_ B -> ( A. x e. a A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) -> A. x e. a A. y e. b ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) )
16 7 13 15 sylc 
 |-  ( ( ( ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ P =/= B ) /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) /\ ( a e. ( LIdeal ` R ) /\ b e. ( LIdeal ` R ) ) ) /\ A. x e. a A. y e. b ( x .x. y ) e. P ) -> A. x e. a A. y e. b ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) )
17 r19.26-2 
 |-  ( A. x e. a A. y e. b ( ( x .x. y ) e. P /\ ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) <-> ( A. x e. a A. y e. b ( x .x. y ) e. P /\ A. x e. a A. y e. b ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) )
18 pm3.35 
 |-  ( ( ( x .x. y ) e. P /\ ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) -> ( x e. P \/ y e. P ) )
19 18 2ralimi 
 |-  ( A. x e. a A. y e. b ( ( x .x. y ) e. P /\ ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) -> A. x e. a A. y e. b ( x e. P \/ y e. P ) )
20 17 19 sylbir 
 |-  ( ( A. x e. a A. y e. b ( x .x. y ) e. P /\ A. x e. a A. y e. b ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) -> A. x e. a A. y e. b ( x e. P \/ y e. P ) )
21 3 16 20 syl2anc 
 |-  ( ( ( ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ P =/= B ) /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) /\ ( a e. ( LIdeal ` R ) /\ b e. ( LIdeal ` R ) ) ) /\ A. x e. a A. y e. b ( x .x. y ) e. P ) -> A. x e. a A. y e. b ( x e. P \/ y e. P ) )
22 2ralor 
 |-  ( A. x e. a A. y e. b ( x e. P \/ y e. P ) <-> ( A. x e. a x e. P \/ A. y e. b y e. P ) )
23 dfss3 
 |-  ( a C_ P <-> A. x e. a x e. P )
24 dfss3 
 |-  ( b C_ P <-> A. y e. b y e. P )
25 23 24 orbi12i 
 |-  ( ( a C_ P \/ b C_ P ) <-> ( A. x e. a x e. P \/ A. y e. b y e. P ) )
26 22 25 sylbb2 
 |-  ( A. x e. a A. y e. b ( x e. P \/ y e. P ) -> ( a C_ P \/ b C_ P ) )
27 21 26 syl 
 |-  ( ( ( ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ P =/= B ) /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) /\ ( a e. ( LIdeal ` R ) /\ b e. ( LIdeal ` R ) ) ) /\ A. x e. a A. y e. b ( x .x. y ) e. P ) -> ( a C_ P \/ b C_ P ) )
28 27 ex 
 |-  ( ( ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ P =/= B ) /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) /\ ( a e. ( LIdeal ` R ) /\ b e. ( LIdeal ` R ) ) ) -> ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) )
29 28 ralrimivva 
 |-  ( ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ P =/= B ) /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) -> 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 ) ) )
30 1 2 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 ) ) ) ) )
31 30 biimpar 
 |-  ( ( R e. Ring /\ ( 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. ( PrmIdeal ` R ) )
32 31 3anassrs 
 |-  ( ( ( ( R e. Ring /\ 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. ( PrmIdeal ` R ) )
33 29 32 syldan 
 |-  ( ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ P =/= B ) /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) -> P e. ( PrmIdeal ` R ) )
34 33 anasss 
 |-  ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ ( P =/= B /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) ) -> P e. ( PrmIdeal ` R ) )