Metamath Proof Explorer

Theorem pridlc3

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 pridlc3 
|- ( ( ( R e. CRingOps /\ P e. ( PrIdl ` R ) ) /\ ( A e. ( X \ P ) /\ B e. ( X \ P ) ) ) -> ( A H B ) e. ( X \ 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 crngorngo 
 |-  ( R e. CRingOps -> R e. RingOps )
5 eldifi 
 |-  ( A e. ( X \ P ) -> A e. X )
6 eldifi 
 |-  ( B e. ( X \ P ) -> B e. X )
7 5 6 anim12i 
 |-  ( ( A e. ( X \ P ) /\ B e. ( X \ P ) ) -> ( A e. X /\ B e. X ) )
8 1 2 3 rngocl 
 |-  ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( A H B ) e. X )
9 8 3expb 
 |-  ( ( R e. RingOps /\ ( A e. X /\ B e. X ) ) -> ( A H B ) e. X )
10 4 7 9 syl2an 
 |-  ( ( R e. CRingOps /\ ( A e. ( X \ P ) /\ B e. ( X \ P ) ) ) -> ( A H B ) e. X )
11 10 adantlr 
 |-  ( ( ( R e. CRingOps /\ P e. ( PrIdl ` R ) ) /\ ( A e. ( X \ P ) /\ B e. ( X \ P ) ) ) -> ( A H B ) e. X )
12 eldifn 
 |-  ( B e. ( X \ P ) -> -. B e. P )
13 12 ad2antll 
 |-  ( ( ( R e. CRingOps /\ P e. ( PrIdl ` R ) ) /\ ( A e. ( X \ P ) /\ B e. ( X \ P ) ) ) -> -. B e. P )
14 1 2 3 pridlc2 
 |-  ( ( ( R e. CRingOps /\ P e. ( PrIdl ` R ) ) /\ ( A e. ( X \ P ) /\ B e. X /\ ( A H B ) e. P ) ) -> B e. P )
15 14 3exp2 
 |-  ( ( R e. CRingOps /\ P e. ( PrIdl ` R ) ) -> ( A e. ( X \ P ) -> ( B e. X -> ( ( A H B ) e. P -> B e. P ) ) ) )
16 15 imp32 
 |-  ( ( ( R e. CRingOps /\ P e. ( PrIdl ` R ) ) /\ ( A e. ( X \ P ) /\ B e. X ) ) -> ( ( A H B ) e. P -> B e. P ) )
17 16 con3d 
 |-  ( ( ( R e. CRingOps /\ P e. ( PrIdl ` R ) ) /\ ( A e. ( X \ P ) /\ B e. X ) ) -> ( -. B e. P -> -. ( A H B ) e. P ) )
18 6 17 sylanr2 
 |-  ( ( ( R e. CRingOps /\ P e. ( PrIdl ` R ) ) /\ ( A e. ( X \ P ) /\ B e. ( X \ P ) ) ) -> ( -. B e. P -> -. ( A H B ) e. P ) )
19 13 18 mpd 
 |-  ( ( ( R e. CRingOps /\ P e. ( PrIdl ` R ) ) /\ ( A e. ( X \ P ) /\ B e. ( X \ P ) ) ) -> -. ( A H B ) e. P )
20 11 19 eldifd 
 |-  ( ( ( R e. CRingOps /\ P e. ( PrIdl ` R ) ) /\ ( A e. ( X \ P ) /\ B e. ( X \ P ) ) ) -> ( A H B ) e. ( X \ P ) )