Metamath Proof Explorer


Theorem mxidln1

Description: One is not contained in any maximal ideal. (Contributed by Jeff Madsen, 17-Jun-2011) (Revised by Thierry Arnoux, 19-Jan-2024)

Ref Expression
Hypotheses mxidlval.1 B = Base R
mxidln1.1 1 ˙ = 1 R
Assertion mxidln1 Could not format assertion : No typesetting found for |- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> -. .1. e. M ) with typecode |-

Proof

Step Hyp Ref Expression
1 mxidlval.1 B = Base R
2 mxidln1.1 1 ˙ = 1 R
3 1 mxidlnr Could not format ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M =/= B ) : No typesetting found for |- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M =/= B ) with typecode |-
4 1 mxidlidl Could not format ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M e. ( LIdeal ` R ) ) with typecode |-
5 eqid LIdeal R = LIdeal R
6 5 1 2 lidl1el R Ring M LIdeal R 1 ˙ M M = B
7 4 6 syldan Could not format ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> ( .1. e. M <-> M = B ) ) : No typesetting found for |- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> ( .1. e. M <-> M = B ) ) with typecode |-
8 7 necon3bbid Could not format ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> ( -. .1. e. M <-> M =/= B ) ) : No typesetting found for |- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> ( -. .1. e. M <-> M =/= B ) ) with typecode |-
9 3 8 mpbird Could not format ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> -. .1. e. M ) : No typesetting found for |- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> -. .1. e. M ) with typecode |-