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 · ˙ = R
Assertion prmidl2 Could not format assertion : No typesetting found for |- ( ( ( 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 ) ) with typecode |-

Proof

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