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{˙}{0} = 0_{R}$
	Assertion	drng0mxidl	$⊢ R \in DivRing \to \{\underset{˙}{0}\} \in MaxIdeal (R)$

Proof

Step	Hyp	Ref	Expression
1		drngmxidl.1	$⊢ \underset{˙}{0} = 0_{R}$
2		drngring	$⊢ R \in DivRing \to R \in Ring$
3		eqid	$⊢ LIdeal (R) = LIdeal (R)$
4	3 1	lidl0	$⊢ R \in Ring \to \{\underset{˙}{0}\} \in LIdeal (R)$
5	2 4	syl	$⊢ R \in DivRing \to \{\underset{˙}{0}\} \in LIdeal (R)$
6		eqid	$⊢ {Base}_{R} = {Base}_{R}$
7		eqid	$⊢ 1_{R} = 1_{R}$
8	6 7	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
9	2 8	syl	$⊢ R \in DivRing \to 1_{R} \in {Base}_{R}$
10		drngnzr	$⊢ R \in DivRing \to R \in NzRing$
11	7 1	nzrnz	$⊢ R \in NzRing \to 1_{R} \neq \underset{˙}{0}$
12		nelsn	$⊢ 1_{R} \neq \underset{˙}{0} \to \neg 1_{R} \in \{\underset{˙}{0}\}$
13	10 11 12	3syl	$⊢ R \in DivRing \to \neg 1_{R} \in \{\underset{˙}{0}\}$
14		nelne1	$⊢ (1_{R} \in {Base}_{R} \land \neg 1_{R} \in \{\underset{˙}{0}\}) \to {Base}_{R} \neq \{\underset{˙}{0}\}$
15	9 13 14	syl2anc	$⊢ R \in DivRing \to {Base}_{R} \neq \{\underset{˙}{0}\}$
16	15	necomd	$⊢ R \in DivRing \to \{\underset{˙}{0}\} \neq {Base}_{R}$
17	6 1 3	drngnidl	$⊢ R \in DivRing \to LIdeal (R) = \{\{\underset{˙}{0}\}, {Base}_{R}\}$
18	17	eleq2d	$⊢ R \in DivRing \to (j \in LIdeal (R) \leftrightarrow j \in \{\{\underset{˙}{0}\}, {Base}_{R}\})$
19	18	biimpa	$⊢ (R \in DivRing \land j \in LIdeal (R)) \to j \in \{\{\underset{˙}{0}\}, {Base}_{R}\}$
20		elpri	$⊢ j \in \{\{\underset{˙}{0}\}, {Base}_{R}\} \to (j = \{\underset{˙}{0}\} \lor j = {Base}_{R})$
21	19 20	syl	$⊢ (R \in DivRing \land j \in LIdeal (R)) \to (j = \{\underset{˙}{0}\} \lor j = {Base}_{R})$
22	21	a1d	$⊢ (R \in DivRing \land j \in LIdeal (R)) \to (\{\underset{˙}{0}\} \subseteq j \to (j = \{\underset{˙}{0}\} \lor j = {Base}_{R}))$
23	22	ralrimiva	$⊢ R \in DivRing \to \forall j \in LIdeal (R) (\{\underset{˙}{0}\} \subseteq j \to (j = \{\underset{˙}{0}\} \lor j = {Base}_{R}))$
24	6	ismxidl	$⊢ R \in Ring \to (\{\underset{˙}{0}\} \in MaxIdeal (R) \leftrightarrow (\{\underset{˙}{0}\} \in LIdeal (R) \land \{\underset{˙}{0}\} \neq {Base}_{R} \land \forall j \in LIdeal (R) (\{\underset{˙}{0}\} \subseteq j \to (j = \{\underset{˙}{0}\} \lor j = {Base}_{R}))))$
25	24	biimpar	$⊢ (R \in Ring \land (\{\underset{˙}{0}\} \in LIdeal (R) \land \{\underset{˙}{0}\} \neq {Base}_{R} \land \forall j \in LIdeal (R) (\{\underset{˙}{0}\} \subseteq j \to (j = \{\underset{˙}{0}\} \lor j = {Base}_{R})))) \to \{\underset{˙}{0}\} \in MaxIdeal (R)$
26	2 5 16 23 25	syl13anc	$⊢ R \in DivRing \to \{\underset{˙}{0}\} \in MaxIdeal (R)$

Metamath Proof Explorer

Theorem drng0mxidl

Proof