Theorem prmidlnr

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

	Ref	Expression
Hypotheses	prmidlval.1	|- B = ( Base ` R )
	prmidlval.2	|- .x. = ( .r ` R )
Assertion	prmidlnr	|- ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) -> P =/= B )

Proof

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