Metamath Proof Explorer

Theorem pridlnr

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

Ref Expression
Hypotheses pridlnr.1 
|- G = ( 1st ` R )
prdilnr.2 
|- X = ran G
Assertion pridlnr 
|- ( ( R e. RingOps /\ P e. ( PrIdl ` R ) ) -> P =/= X )

Proof

Step Hyp Ref Expression
1 pridlnr.1 
 |-  G = ( 1st ` R )
2 prdilnr.2 
 |-  X = ran G
3 eqid 
 |-  ( 2nd ` R ) = ( 2nd ` R )
4 1 3 2 ispridl 
 |-  ( R e. RingOps -> ( P e. ( PrIdl ` R ) <-> ( P e. ( Idl ` R ) /\ P =/= X /\ 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 3anan12 
 |-  ( ( P e. ( Idl ` R ) /\ P =/= X /\ 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 =/= X /\ ( P e. ( Idl ` 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 =/= X /\ ( P e. ( Idl ` 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 =/= X )