Metamath Proof Explorer

Theorem pridlidl

Description: A prime ideal is an ideal. (Contributed by Jeff Madsen, 19-Jun-2010)

Ref Expression
Assertion pridlidl 
|- ( ( R e. RingOps /\ P e. ( PrIdl ` R ) ) -> P e. ( Idl ` R ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( 1st ` R ) = ( 1st ` R )
2 eqid 
 |-  ( 2nd ` R ) = ( 2nd ` R )
3 eqid 
 |-  ran ( 1st ` R ) = ran ( 1st ` R )
4 1 2 3 ispridl 
 |-  ( R e. RingOps -> ( P e. ( PrIdl ` R ) <-> ( P e. ( Idl ` R ) /\ P =/= ran ( 1st ` R ) /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x ( 2nd ` R ) y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) )
5 3anass 
 |-  ( ( P e. ( Idl ` R ) /\ P =/= ran ( 1st ` R ) /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x ( 2nd ` R ) y ) e. P -> ( a C_ P \/ b C_ P ) ) ) <-> ( P e. ( Idl ` R ) /\ ( P =/= ran ( 1st ` R ) /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x ( 2nd ` R ) y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) )
6 4 5 bitrdi 
 |-  ( R e. RingOps -> ( P e. ( PrIdl ` R ) <-> ( P e. ( Idl ` R ) /\ ( P =/= ran ( 1st ` R ) /\ A. a e. ( Idl ` R ) A. b e. ( Idl ` R ) ( A. x e. a A. y e. b ( x ( 2nd ` R ) y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) ) )
7 6 simprbda 
 |-  ( ( R e. RingOps /\ P e. ( PrIdl ` R ) ) -> P e. ( Idl ` R ) )