Metamath Proof Explorer

Theorem prmidlidl

Description: A prime ideal is an ideal. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Thierry Arnoux, 12-Jan-2024)

Ref Expression
Assertion prmidlidl 
|- ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) -> P e. ( LIdeal ` R ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` R ) = ( Base ` R )
2 eqid 
 |-  ( .r ` R ) = ( .r ` R )
3 1 2 isprmidl 
 |-  ( R e. Ring -> ( P e. ( PrmIdeal ` R ) <-> ( P e. ( LIdeal ` R ) /\ P =/= ( Base ` R ) /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x ( .r ` R ) y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) )
4 3 biimpa 
 |-  ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) -> ( P e. ( LIdeal ` R ) /\ P =/= ( Base ` R ) /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x ( .r ` R ) y ) e. P -> ( a C_ P \/ b C_ P ) ) ) )
5 4 simp1d 
 |-  ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) -> P e. ( LIdeal ` R ) )