drngmxidl

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

		Ref	Expression
	Hypothesis	drngmxidl.1	$⊢ \underset{˙}{0} = 0_{R}$
	Assertion	drngmxidl	$⊢ R \in DivRing \to MaxIdeal (R) = \{\{\underset{˙}{0}\}\}$

Proof

Step	Hyp	Ref	Expression
1		drngmxidl.1	$⊢ \underset{˙}{0} = 0_{R}$
2		drngring	$⊢ R \in DivRing \to R \in Ring$
3		eqid	$⊢ {Base}_{R} = {Base}_{R}$
4	3	mxidlidl	$⊢ (R \in Ring \land i \in MaxIdeal (R)) \to i \in LIdeal (R)$
5	4	ex	$⊢ R \in Ring \to (i \in MaxIdeal (R) \to i \in LIdeal (R))$
6	5	ssrdv	$⊢ R \in Ring \to MaxIdeal (R) \subseteq LIdeal (R)$
7	2 6	syl	$⊢ R \in DivRing \to MaxIdeal (R) \subseteq LIdeal (R)$
8		eqid	$⊢ LIdeal (R) = LIdeal (R)$
9	3 1 8	drngnidl	$⊢ R \in DivRing \to LIdeal (R) = \{\{\underset{˙}{0}\}, {Base}_{R}\}$
10	7 9	sseqtrd	$⊢ R \in DivRing \to MaxIdeal (R) \subseteq \{\{\underset{˙}{0}\}, {Base}_{R}\}$
11	3	mxidlnr	$⊢ (R \in Ring \land i \in MaxIdeal (R)) \to i \neq {Base}_{R}$
12	2 11	sylan	$⊢ (R \in DivRing \land i \in MaxIdeal (R)) \to i \neq {Base}_{R}$
13	12	nelrdva	$⊢ R \in DivRing \to \neg {Base}_{R} \in MaxIdeal (R)$
14		ssdifsn	$⊢ MaxIdeal (R) \subseteq \{\{\underset{˙}{0}\}, {Base}_{R}\} ∖ \{{Base}_{R}\} \leftrightarrow (MaxIdeal (R) \subseteq \{\{\underset{˙}{0}\}, {Base}_{R}\} \land \neg {Base}_{R} \in MaxIdeal (R))$
15	10 13 14	sylanbrc	$⊢ R \in DivRing \to MaxIdeal (R) \subseteq \{\{\underset{˙}{0}\}, {Base}_{R}\} ∖ \{{Base}_{R}\}$
16		drngnzr	$⊢ R \in DivRing \to R \in NzRing$
17	1 3	drnglidl1ne0	$⊢ R \in NzRing \to {Base}_{R} \neq \{\underset{˙}{0}\}$
18	17	necomd	$⊢ R \in NzRing \to \{\underset{˙}{0}\} \neq {Base}_{R}$
19		difprsn2	$⊢ \{\underset{˙}{0}\} \neq {Base}_{R} \to \{\{\underset{˙}{0}\}, {Base}_{R}\} ∖ \{{Base}_{R}\} = \{\{\underset{˙}{0}\}\}$
20	16 18 19	3syl	$⊢ R \in DivRing \to \{\{\underset{˙}{0}\}, {Base}_{R}\} ∖ \{{Base}_{R}\} = \{\{\underset{˙}{0}\}\}$
21	15 20	sseqtrd	$⊢ R \in DivRing \to MaxIdeal (R) \subseteq \{\{\underset{˙}{0}\}\}$
22	1	drng0mxidl	$⊢ R \in DivRing \to \{\underset{˙}{0}\} \in MaxIdeal (R)$
23	22	snssd	$⊢ R \in DivRing \to \{\{\underset{˙}{0}\}\} \subseteq MaxIdeal (R)$
24	21 23	eqssd	$⊢ R \in DivRing \to MaxIdeal (R) = \{\{\underset{˙}{0}\}\}$

Metamath Proof Explorer

Theorem drngmxidl

Proof