Metamath Proof Explorer


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

Proof

Step Hyp Ref Expression
1 prmidlval.1 B = Base R
2 prmidlval.2 · ˙ = R
3 1 2 isprmidl Could not format ( 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 ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) with typecode |-
4 3 biimpa Could not format ( ( 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 ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) with typecode |-
5 4 simp2d Could not format ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) -> P =/= B ) : No typesetting found for |- ( ( R e. Ring /\ P e. ( PrmIdeal ` R ) ) -> P =/= B ) with typecode |-