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 · ˙ = R
Assertion isprmidl Could not format assertion : 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 |-

Proof

Step Hyp Ref Expression
1 prmidlval.1 B = Base R
2 prmidlval.2 · ˙ = R
3 1 2 prmidlval Could not format ( 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 ) ) ) } ) : No typesetting found for |- ( 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 ) ) ) } ) with typecode |-
4 3 eleq2d Could not format ( 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 ) ) ) } ) ) : No typesetting found for |- ( 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 ) ) ) } ) ) with typecode |-
5 neeq1 i = P i B P B
6 eleq2 i = P x · ˙ y i x · ˙ y P
7 6 2ralbidv i = P x a y b x · ˙ y i x a y b x · ˙ y P
8 sseq2 i = P a i a P
9 sseq2 i = P b i b P
10 8 9 orbi12d i = P a i b i a P b P
11 7 10 imbi12d i = P x a y b x · ˙ y i a i b i x a y b x · ˙ y P a P b P
12 11 2ralbidv i = P a LIdeal R b LIdeal R x a y b x · ˙ y i a i b i a LIdeal R b LIdeal R x a y b x · ˙ y P a P b P
13 5 12 anbi12d i = P i B a LIdeal R b LIdeal R x a y b x · ˙ y i a i b i P B a LIdeal R b LIdeal R x a y b x · ˙ y P a P b P
14 13 elrab P i LIdeal R | i B a LIdeal R b LIdeal R x a y b x · ˙ y i a i b i P LIdeal R P B a LIdeal R b LIdeal R x a y b x · ˙ y P a P b P
15 4 14 bitrdi 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 |-
16 3anass P LIdeal R P B a LIdeal R b LIdeal R x a y b x · ˙ y P a P b P P LIdeal R P B a LIdeal R b LIdeal R x a y b x · ˙ y P a P b P
17 15 16 bitr4di 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 |-