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=BaseR
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=BaseR
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=PiBPB
6 eleq2 i=Px·˙yix·˙yP
7 6 2ralbidv i=Pxaybx·˙yixaybx·˙yP
8 sseq2 i=PaiaP
9 sseq2 i=PbibP
10 8 9 orbi12d i=PaibiaPbP
11 7 10 imbi12d i=Pxaybx·˙yiaibixaybx·˙yPaPbP
12 11 2ralbidv i=PaLIdealRbLIdealRxaybx·˙yiaibiaLIdealRbLIdealRxaybx·˙yPaPbP
13 5 12 anbi12d i=PiBaLIdealRbLIdealRxaybx·˙yiaibiPBaLIdealRbLIdealRxaybx·˙yPaPbP
14 13 elrab PiLIdealR|iBaLIdealRbLIdealRxaybx·˙yiaibiPLIdealRPBaLIdealRbLIdealRxaybx·˙yPaPbP
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 PLIdealRPBaLIdealRbLIdealRxaybx·˙yPaPbPPLIdealRPBaLIdealRbLIdealRxaybx·˙yPaPbP
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 |-