Metamath Proof Explorer

Theorem prmidlc2

Description: Property of a prime ideal in a commutative ring. (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 prmidlc2 
|- ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( B \ P ) /\ J e. B /\ ( I .x. J ) e. P ) ) -> J e. P )

Proof

Step Hyp Ref Expression
1 isprmidlc.1 
 |-  B = ( Base ` R )
2 isprmidlc.2 
 |-  .x. = ( .r ` R )
3 eldifn 
 |-  ( I e. ( B \ P ) -> -. I e. P )
4 3 3ad2ant1 
 |-  ( ( I e. ( B \ P ) /\ J e. B /\ ( I .x. J ) e. P ) -> -. I e. P )
5 4 adantl 
 |-  ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( B \ P ) /\ J e. B /\ ( I .x. J ) e. P ) ) -> -. I e. P )
6 eldifi 
 |-  ( I e. ( B \ P ) -> I e. B )
7 1 2 prmidlc 
 |-  ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. B /\ J e. B /\ ( I .x. J ) e. P ) ) -> ( I e. P \/ J e. P ) )
8 7 ord 
 |-  ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. B /\ J e. B /\ ( I .x. J ) e. P ) ) -> ( -. I e. P -> J e. P ) )
9 6 8 syl3anr1 
 |-  ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( B \ P ) /\ J e. B /\ ( I .x. J ) e. P ) ) -> ( -. I e. P -> J e. P ) )
10 5 9 mpd 
 |-  ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. ( B \ P ) /\ J e. B /\ ( I .x. J ) e. P ) ) -> J e. P )