This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pridlc2

Description: Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011)

Ref Expression
Hypotheses ispridlc.1 
|- G = ( 1st ` R )
ispridlc.2 
|- H = ( 2nd ` R )
ispridlc.3 
|- X = ran G
Assertion pridlc2 
|- ( ( ( R e. CRingOps /\ P e. ( PrIdl ` R ) ) /\ ( A e. ( X \ P ) /\ B e. X /\ ( A H B ) e. P ) ) -> B e. P )

Proof

Step Hyp Ref Expression
1 ispridlc.1 
 |-  G = ( 1st ` R )
2 ispridlc.2 
 |-  H = ( 2nd ` R )
3 ispridlc.3 
 |-  X = ran G
4 eldifn 
 |-  ( A e. ( X \ P ) -> -. A e. P )
5 4 3ad2ant1 
 |-  ( ( A e. ( X \ P ) /\ B e. X /\ ( A H B ) e. P ) -> -. A e. P )
6 5 adantl 
 |-  ( ( ( R e. CRingOps /\ P e. ( PrIdl ` R ) ) /\ ( A e. ( X \ P ) /\ B e. X /\ ( A H B ) e. P ) ) -> -. A e. P )
7 eldifi 
 |-  ( A e. ( X \ P ) -> A e. X )
8 1 2 3 pridlc 
 |-  ( ( ( R e. CRingOps /\ P e. ( PrIdl ` R ) ) /\ ( A e. X /\ B e. X /\ ( A H B ) e. P ) ) -> ( A e. P \/ B e. P ) )
9 8 ord 
 |-  ( ( ( R e. CRingOps /\ P e. ( PrIdl ` R ) ) /\ ( A e. X /\ B e. X /\ ( A H B ) e. P ) ) -> ( -. A e. P -> B e. P ) )
10 7 9 syl3anr1 
 |-  ( ( ( R e. CRingOps /\ P e. ( PrIdl ` R ) ) /\ ( A e. ( X \ P ) /\ B e. X /\ ( A H B ) e. P ) ) -> ( -. A e. P -> B e. P ) )
11 6 10 mpd 
 |-  ( ( ( R e. CRingOps /\ P e. ( PrIdl ` R ) ) /\ ( A e. ( X \ P ) /\ B e. X /\ ( A H B ) e. P ) ) -> B e. P )