Theorem drng0mxidl

Description: In a division ring, the zero ideal is a maximal ideal. (Contributed by Thierry Arnoux, 16-Mar-2025)

	Ref	Expression
Hypothesis	drngmxidl.1	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	drng0mxidl	Could not format assertion : No typesetting found for |- ( R e. DivRing -> { .0. } e. ( MaxIdeal ` R ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		drngmxidl.1	$$⊢\underset{\dot{}}{0}=0_R$$
2		drngring	$$⊢R\in \mathrm{DivRing}\to R\in \mathrm{Ring}$$
3		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
4	3 1	lidl0	$$⊢R\in \mathrm{Ring}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{LIdeal}\left(R\right)$$
5	2 4	syl	$$⊢R\in \mathrm{DivRing}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{LIdeal}\left(R\right)$$
6		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
7		eqid	$$⊢1_R=1_R$$
8	6 7	ringidcl	$$⊢R\in \mathrm{Ring}\to 1_R\in {\mathrm{Base}}_R$$
9	2 8	syl	$$⊢R\in \mathrm{DivRing}\to 1_R\in {\mathrm{Base}}_R$$
10		drngnzr	$$⊢R\in \mathrm{DivRing}\to R\in \mathrm{NzRing}$$
11	7 1	nzrnz	$$⊢R\in \mathrm{NzRing}\to 1_R\ne \underset{\dot{}}{0}$$
12		nelsn	$$⊢1_R\ne \underset{\dot{}}{0}\to \neg 1_R\in \left\{\underset{\dot{}}{0}\right\}$$
13	10 11 12	3syl	$$⊢R\in \mathrm{DivRing}\to \neg 1_R\in \left\{\underset{\dot{}}{0}\right\}$$
14		nelne1	$$⊢\left(1_R\in {\mathrm{Base}}_R\wedge \neg 1_R\in \left\{\underset{\dot{}}{0}\right\}\right)\to {\mathrm{Base}}_R\ne \left\{\underset{\dot{}}{0}\right\}$$
15	9 13 14	syl2anc	$$⊢R\in \mathrm{DivRing}\to {\mathrm{Base}}_R\ne \left\{\underset{\dot{}}{0}\right\}$$
16	15	necomd	$$⊢R\in \mathrm{DivRing}\to \left\{\underset{\dot{}}{0}\right\}\ne {\mathrm{Base}}_R$$
17	6 1 3	drngnidl	$$⊢R\in \mathrm{DivRing}\to \mathrm{LIdeal}\left(R\right)=\left\{\left\{\underset{\dot{}}{0}\right\},{\mathrm{Base}}_R\right\}$$
18	17	eleq2d	$$⊢R\in \mathrm{DivRing}\to \left(j\in \mathrm{LIdeal}\left(R\right)\leftrightarrow j\in \left\{\left\{\underset{\dot{}}{0}\right\},{\mathrm{Base}}_R\right\}\right)$$
19	18	biimpa	$$⊢\left(R\in \mathrm{DivRing}\wedge j\in \mathrm{LIdeal}\left(R\right)\right)\to j\in \left\{\left\{\underset{\dot{}}{0}\right\},{\mathrm{Base}}_R\right\}$$
20		elpri	$$⊢j\in \left\{\left\{\underset{\dot{}}{0}\right\},{\mathrm{Base}}_R\right\}\to \left(j=\left\{\underset{\dot{}}{0}\right\}\vee j={\mathrm{Base}}_R\right)$$
21	19 20	syl	$$⊢\left(R\in \mathrm{DivRing}\wedge j\in \mathrm{LIdeal}\left(R\right)\right)\to \left(j=\left\{\underset{\dot{}}{0}\right\}\vee j={\mathrm{Base}}_R\right)$$
22	21	a1d	$$⊢\left(R\in \mathrm{DivRing}\wedge j\in \mathrm{LIdeal}\left(R\right)\right)\to \left(\left\{\underset{\dot{}}{0}\right\}\subseteq j\to \left(j=\left\{\underset{\dot{}}{0}\right\}\vee j={\mathrm{Base}}_R\right)\right)$$
23	22	ralrimiva	$$⊢R\in \mathrm{DivRing}\to \forall j\in \mathrm{LIdeal}\left(R\right)\left(\left\{\underset{\dot{}}{0}\right\}\subseteq j\to \left(j=\left\{\underset{\dot{}}{0}\right\}\vee j={\mathrm{Base}}_R\right)\right)$$
24	6	ismxidl	Could not format ( R e. Ring -> ( { .0. } e. ( MaxIdeal ` R ) <-> ( { .0. } e. ( LIdeal ` R ) /\ { .0. } =/= ( Base ` R ) /\ A. j e. ( LIdeal ` R ) ( { .0. } C_ j -> ( j = { .0. } \/ j = ( Base ` R ) ) ) ) ) ) : No typesetting found for |- ( R e. Ring -> ( { .0. } e. ( MaxIdeal ` R ) <-> ( { .0. } e. ( LIdeal ` R ) /\ { .0. } =/= ( Base ` R ) /\ A. j e. ( LIdeal ` R ) ( { .0. } C_ j -> ( j = { .0. } \/ j = ( Base ` R ) ) ) ) ) ) with typecode |-
25	24	biimpar	Could not format ( ( R e. Ring /\ ( { .0. } e. ( LIdeal ` R ) /\ { .0. } =/= ( Base ` R ) /\ A. j e. ( LIdeal ` R ) ( { .0. } C_ j -> ( j = { .0. } \/ j = ( Base ` R ) ) ) ) ) -> { .0. } e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ ( { .0. } e. ( LIdeal ` R ) /\ { .0. } =/= ( Base ` R ) /\ A. j e. ( LIdeal ` R ) ( { .0. } C_ j -> ( j = { .0. } \/ j = ( Base ` R ) ) ) ) ) -> { .0. } e. ( MaxIdeal ` R ) ) with typecode |-
26	2 5 16 23 25	syl13anc	Could not format ( R e. DivRing -> { .0. } e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( R e. DivRing -> { .0. } e. ( MaxIdeal ` R ) ) with typecode |-