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	Could not format assertion : No typesetting found for |- ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) -> P e. ( LIdeal ` R ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
2		eqid	$$⊢{\cdot }_R={\cdot }_R$$
3	1 2	isprmidl	Could not format ( 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 ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) with typecode |-
4	3	biimpa	Could not format ( ( 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 ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) with typecode |-
5	4	simp1d	Could not format ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) -> P e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) -> P e. ( LIdeal ` R ) ) with typecode |-