drngmxidlr

Description: If a ring's only maximal ideal is the zero ideal, it is a division ring. See also drngmxidl . (Contributed by Thierry Arnoux, 3-Jun-2025)

	Ref	Expression
Hypotheses	drngmxidlr.b	$⊢ B = {Base}_{R}$
	drngmxidlr.z	$⊢ \underset{˙}{0} = 0_{R}$
	drngmxidlr.u	$⊢ M = MaxIdeal (R)$
	drngmxidlr.r	$⊢ φ \to R \in NzRing$
	drngmxidlr.2	$⊢ φ \to M = \{\{\underset{˙}{0}\}\}$
Assertion	drngmxidlr	$⊢ φ \to R \in DivRing$

Proof

Step	Hyp	Ref	Expression
1		drngmxidlr.b	$⊢ B = {Base}_{R}$
2		drngmxidlr.z	$⊢ \underset{˙}{0} = 0_{R}$
3		drngmxidlr.u	$⊢ M = MaxIdeal (R)$
4		drngmxidlr.r	$⊢ φ \to R \in NzRing$
5		drngmxidlr.2	$⊢ φ \to M = \{\{\underset{˙}{0}\}\}$
6		simpr	$⊢ ((((φ \land i \in LIdeal (R)) \land i \neq B) \land m \in MaxIdeal (R)) \land i \subseteq m) \to i \subseteq m$
7		simplr	$⊢ ((((φ \land i \in LIdeal (R)) \land i \neq B) \land m \in MaxIdeal (R)) \land i \subseteq m) \to m \in MaxIdeal (R)$
8	7 3	eleqtrrdi	$⊢ ((((φ \land i \in LIdeal (R)) \land i \neq B) \land m \in MaxIdeal (R)) \land i \subseteq m) \to m \in M$
9	5	ad4antr	$⊢ ((((φ \land i \in LIdeal (R)) \land i \neq B) \land m \in MaxIdeal (R)) \land i \subseteq m) \to M = \{\{\underset{˙}{0}\}\}$
10	8 9	eleqtrd	$⊢ ((((φ \land i \in LIdeal (R)) \land i \neq B) \land m \in MaxIdeal (R)) \land i \subseteq m) \to m \in \{\{\underset{˙}{0}\}\}$
11		elsni	$⊢ m \in \{\{\underset{˙}{0}\}\} \to m = \{\underset{˙}{0}\}$
12	10 11	syl	$⊢ ((((φ \land i \in LIdeal (R)) \land i \neq B) \land m \in MaxIdeal (R)) \land i \subseteq m) \to m = \{\underset{˙}{0}\}$
13	6 12	sseqtrd	$⊢ ((((φ \land i \in LIdeal (R)) \land i \neq B) \land m \in MaxIdeal (R)) \land i \subseteq m) \to i \subseteq \{\underset{˙}{0}\}$
14		nzrring	$⊢ R \in NzRing \to R \in Ring$
15	4 14	syl	$⊢ φ \to R \in Ring$
16		eqid	$⊢ LIdeal (R) = LIdeal (R)$
17	16 2	lidl0cl	$⊢ (R \in Ring \land i \in LIdeal (R)) \to \underset{˙}{0} \in i$
18	15 17	sylan	$⊢ (φ \land i \in LIdeal (R)) \to \underset{˙}{0} \in i$
19	18	snssd	$⊢ (φ \land i \in LIdeal (R)) \to \{\underset{˙}{0}\} \subseteq i$
20	19	ad5ant12	$⊢ ((((φ \land i \in LIdeal (R)) \land i \neq B) \land m \in MaxIdeal (R)) \land i \subseteq m) \to \{\underset{˙}{0}\} \subseteq i$
21	13 20	eqssd	$⊢ ((((φ \land i \in LIdeal (R)) \land i \neq B) \land m \in MaxIdeal (R)) \land i \subseteq m) \to i = \{\underset{˙}{0}\}$
22	15	ad2antrr	$⊢ ((φ \land i \in LIdeal (R)) \land i \neq B) \to R \in Ring$
23		simplr	$⊢ ((φ \land i \in LIdeal (R)) \land i \neq B) \to i \in LIdeal (R)$
24		simpr	$⊢ ((φ \land i \in LIdeal (R)) \land i \neq B) \to i \neq B$
25	1	ssmxidl	$⊢ (R \in Ring \land i \in LIdeal (R) \land i \neq B) \to \exists m \in MaxIdeal (R) i \subseteq m$
26	22 23 24 25	syl3anc	$⊢ ((φ \land i \in LIdeal (R)) \land i \neq B) \to \exists m \in MaxIdeal (R) i \subseteq m$
27	21 26	r19.29a	$⊢ ((φ \land i \in LIdeal (R)) \land i \neq B) \to i = \{\underset{˙}{0}\}$
28		simpr	$⊢ ((φ \land i \in LIdeal (R)) \land i = B) \to i = B$
29		exmidne	$⊢ (i = B \lor i \neq B)$
30	29	a1i	$⊢ (φ \land i \in LIdeal (R)) \to (i = B \lor i \neq B)$
31	30	orcomd	$⊢ (φ \land i \in LIdeal (R)) \to (i \neq B \lor i = B)$
32	27 28 31	orim12da	$⊢ (φ \land i \in LIdeal (R)) \to (i = \{\underset{˙}{0}\} \lor i = B)$
33		vex	$⊢ i \in V$
34	33	elpr	$⊢ i \in \{\{\underset{˙}{0}\}, B\} \leftrightarrow (i = \{\underset{˙}{0}\} \lor i = B)$
35	32 34	sylibr	$⊢ (φ \land i \in LIdeal (R)) \to i \in \{\{\underset{˙}{0}\}, B\}$
36	35	ex	$⊢ φ \to (i \in LIdeal (R) \to i \in \{\{\underset{˙}{0}\}, B\})$
37	36	ssrdv	$⊢ φ \to LIdeal (R) \subseteq \{\{\underset{˙}{0}\}, B\}$
38	16 2	lidl0	$⊢ R \in Ring \to \{\underset{˙}{0}\} \in LIdeal (R)$
39	15 38	syl	$⊢ φ \to \{\underset{˙}{0}\} \in LIdeal (R)$
40	16 1	lidl1	$⊢ R \in Ring \to B \in LIdeal (R)$
41	15 40	syl	$⊢ φ \to B \in LIdeal (R)$
42	39 41	prssd	$⊢ φ \to \{\{\underset{˙}{0}\}, B\} \subseteq LIdeal (R)$
43	37 42	eqssd	$⊢ φ \to LIdeal (R) = \{\{\underset{˙}{0}\}, B\}$
44	1 2 16	drngidl	$⊢ R \in NzRing \to (R \in DivRing \leftrightarrow LIdeal (R) = \{\{\underset{˙}{0}\}, B\})$
45	4 44	syl	$⊢ φ \to (R \in DivRing \leftrightarrow LIdeal (R) = \{\{\underset{˙}{0}\}, B\})$
46	43 45	mpbird	$⊢ φ \to R \in DivRing$

Metamath Proof Explorer

Theorem drngmxidlr

Proof