Metamath Proof Explorer

Theorem cmprmidlmcl

Description: The complement of a prime ideal is multiplicatively closed. (Contributed by Jeff Madsen, 17-Jun-2011) (Revised by AV, 12-Jul-2026)

Ref Expression
Hypotheses isprmidlc.1 
|- B = ( Base ` R )
isprmidlc.2 
|- .x. = ( .r ` R )
Assertion cmprmidlmcl 
|- ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( B \ P ) /\ J e. ( B \ P ) ) ) -> ( I .x. J ) e. ( B \ P ) )

Proof

Step Hyp Ref Expression
1 isprmidlc.1 
 |-  B = ( Base ` R )
2 isprmidlc.2 
 |-  .x. = ( .r ` R )
3 crngring 
 |-  ( R e. CRing -> R e. Ring )
4 eldifi 
 |-  ( I e. ( B \ P ) -> I e. B )
5 eldifi 
 |-  ( J e. ( B \ P ) -> J e. B )
6 4 5 anim12i 
 |-  ( ( I e. ( B \ P ) /\ J e. ( B \ P ) ) -> ( I e. B /\ J e. B ) )
7 1 2 ringcl 
 |-  ( ( R e. Ring /\ I e. B /\ J e. B ) -> ( I .x. J ) e. B )
8 7 3expb 
 |-  ( ( R e. Ring /\ ( I e. B /\ J e. B ) ) -> ( I .x. J ) e. B )
9 3 6 8 syl2an 
 |-  ( ( R e. CRing /\ ( I e. ( B \ P ) /\ J e. ( B \ P ) ) ) -> ( I .x. J ) e. B )
10 9 adantlr 
 |-  ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( B \ P ) /\ J e. ( B \ P ) ) ) -> ( I .x. J ) e. B )
11 eldifn 
 |-  ( J e. ( B \ P ) -> -. J e. P )
12 11 ad2antll 
 |-  ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( B \ P ) /\ J e. ( B \ P ) ) ) -> -. J e. P )
13 1 2 prmidlc2 
 |-  ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( B \ P ) /\ J e. B /\ ( I .x. J ) e. P ) ) -> J e. P )
14 13 3exp2 
 |-  ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) -> ( I e. ( B \ P ) -> ( J e. B -> ( ( I .x. J ) e. P -> J e. P ) ) ) )
15 14 imp32 
 |-  ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( B \ P ) /\ J e. B ) ) -> ( ( I .x. J ) e. P -> J e. P ) )
16 15 con3d 
 |-  ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( B \ P ) /\ J e. B ) ) -> ( -. J e. P -> -. ( I .x. J ) e. P ) )
17 5 16 sylanr2 
 |-  ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( B \ P ) /\ J e. ( B \ P ) ) ) -> ( -. J e. P -> -. ( I .x. J ) e. P ) )
18 12 17 mpd 
 |-  ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( B \ P ) /\ J e. ( B \ P ) ) ) -> -. ( I .x. J ) e. P )
19 10 18 eldifd 
 |-  ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( B \ P ) /\ J e. ( B \ P ) ) ) -> ( I .x. J ) e. ( B \ P ) )