Theorem mxidlnzr

Description: A ring with a maximal ideal is a nonzero ring. (Contributed by Jeff Madsen, 17-Jun-2011) (Revised by Thierry Arnoux, 19-Jan-2024)

	Ref	Expression
Hypothesis	mxidlval.1	$$⊢B={\mathrm{Base}}_R$$
Assertion	mxidlnzr	Could not format assertion : No typesetting found for |- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> R e. NzRing ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mxidlval.1	$$⊢B={\mathrm{Base}}_R$$
2	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 |-
3		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
4		eqid	$$⊢0_R=0_R$$
5	3 4	lidl0cl	$$⊢\left(R\in \mathrm{Ring}\wedge M\in \mathrm{LIdeal}\left(R\right)\right)\to 0_R\in M$$
6	2 5	syldan	Could not format ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> ( 0g ` R ) e. M ) : No typesetting found for |- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> ( 0g ` R ) e. M ) with typecode |-
7		eqid	$$⊢1_R=1_R$$
8	1 7	mxidln1	Could not format ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> -. ( 1r ` R ) e. M ) : No typesetting found for |- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> -. ( 1r ` R ) e. M ) with typecode |-
9		nelne2	$$⊢\left(0_R\in M\wedge \neg 1_R\in M\right)\to 0_R\ne 1_R$$
10	6 8 9	syl2anc	Could not format ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> ( 0g ` R ) =/= ( 1r ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> ( 0g ` R ) =/= ( 1r ` R ) ) with typecode |-
11	10	necomd	Could not format ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> ( 1r ` R ) =/= ( 0g ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> ( 1r ` R ) =/= ( 0g ` R ) ) with typecode |-
12	7 4	isnzr	$$⊢R\in \mathrm{NzRing}\leftrightarrow \left(R\in \mathrm{Ring}\wedge 1_R\ne 0_R\right)$$
13	12	biimpri	$$⊢\left(R\in \mathrm{Ring}\wedge 1_R\ne 0_R\right)\to R\in \mathrm{NzRing}$$
14	11 13	syldan	Could not format ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> R e. NzRing ) : No typesetting found for |- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> R e. NzRing ) with typecode |-