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={\mathrm{Base}}_R$$
	mxidln1.1	$$⊢\underset{\dot{}}{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={\mathrm{Base}}_R$$
2		mxidln1.1	$$⊢\underset{\dot{}}{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	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
6	5 1 2	lidl1el	$$⊢\left(R\in \mathrm{Ring}\wedge M\in \mathrm{LIdeal}\left(R\right)\right)\to \left(\underset{\dot{}}{1}\in M\leftrightarrow M=B\right)$$
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 |-