dflring3

Description: Alternate definition of a local ring: local rings have a single maximal ideal. (Contributed by Thierry Arnoux, 2-Jun-2026)

		Ref	Expression
	Assertion	dflring3	$⊢ R \in CRing \to (R \in LRing \leftrightarrow MaxIdeal (R) \approx 1_{𝑜})$

Proof

Step	Hyp	Ref	Expression
1		crngring	$⊢ R \in CRing \to R \in Ring$
2	1	adantr	$⊢ (R \in CRing \land R \in LRing) \to R \in Ring$
3	2	adantr	$⊢ ((R \in CRing \land R \in LRing) \land m \in MaxIdeal (R)) \to R \in Ring$
4		simpr	$⊢ ((R \in CRing \land R \in LRing) \land m \in MaxIdeal (R)) \to m \in MaxIdeal (R)$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6		eqid	$⊢ Unit (R) = Unit (R)$
7		simpl	$⊢ (R \in CRing \land R \in LRing) \to R \in CRing$
8		simpr	$⊢ (R \in CRing \land R \in LRing) \to R \in LRing$
9	5 6 7 8	dflringlem2	$⊢ (R \in CRing \land R \in LRing) \to {Base}_{R} ∖ Unit (R) \in LIdeal (R)$
10	9	adantr	$⊢ ((R \in CRing \land R \in LRing) \land m \in MaxIdeal (R)) \to {Base}_{R} ∖ Unit (R) \in LIdeal (R)$
11	5	mxidlidl	$⊢ (R \in Ring \land m \in MaxIdeal (R)) \to m \in LIdeal (R)$
12	2 11	sylan	$⊢ ((R \in CRing \land R \in LRing) \land m \in MaxIdeal (R)) \to m \in LIdeal (R)$
13		eqid	$⊢ LIdeal (R) = LIdeal (R)$
14	5 13	lidlss	$⊢ m \in LIdeal (R) \to m \subseteq {Base}_{R}$
15	12 14	syl	$⊢ ((R \in CRing \land R \in LRing) \land m \in MaxIdeal (R)) \to m \subseteq {Base}_{R}$
16	15	adantr	$⊢ (((R \in CRing \land R \in LRing) \land m \in MaxIdeal (R)) \land \neg m \subseteq {Base}_{R} ∖ Unit (R)) \to m \subseteq {Base}_{R}$
17	16	sselda	$⊢ ((((R \in CRing \land R \in LRing) \land m \in MaxIdeal (R)) \land \neg m \subseteq {Base}_{R} ∖ Unit (R)) \land x \in m) \to x \in {Base}_{R}$
18		neldif	$⊢ (x \in {Base}_{R} \land \neg x \in ({Base}_{R} ∖ Unit (R))) \to x \in Unit (R)$
19	17 18	sylan	$⊢ (((((R \in CRing \land R \in LRing) \land m \in MaxIdeal (R)) \land \neg m \subseteq {Base}_{R} ∖ Unit (R)) \land x \in m) \land \neg x \in ({Base}_{R} ∖ Unit (R))) \to x \in Unit (R)$
20		simplr	$⊢ (((((R \in CRing \land R \in LRing) \land m \in MaxIdeal (R)) \land \neg m \subseteq {Base}_{R} ∖ Unit (R)) \land x \in m) \land \neg x \in ({Base}_{R} ∖ Unit (R))) \to x \in m$
21	2	ad4antr	$⊢ (((((R \in CRing \land R \in LRing) \land m \in MaxIdeal (R)) \land \neg m \subseteq {Base}_{R} ∖ Unit (R)) \land x \in m) \land \neg x \in ({Base}_{R} ∖ Unit (R))) \to R \in Ring$
22	12	ad3antrrr	$⊢ (((((R \in CRing \land R \in LRing) \land m \in MaxIdeal (R)) \land \neg m \subseteq {Base}_{R} ∖ Unit (R)) \land x \in m) \land \neg x \in ({Base}_{R} ∖ Unit (R))) \to m \in LIdeal (R)$
23	5 6 19 20 21 22	lidlunitel	$⊢ (((((R \in CRing \land R \in LRing) \land m \in MaxIdeal (R)) \land \neg m \subseteq {Base}_{R} ∖ Unit (R)) \land x \in m) \land \neg x \in ({Base}_{R} ∖ Unit (R))) \to m = {Base}_{R}$
24		nssrex	$⊢ \neg m \subseteq {Base}_{R} ∖ Unit (R) \leftrightarrow \exists x \in m \neg x \in ({Base}_{R} ∖ Unit (R))$
25	24	bilani	$⊢ (((R \in CRing \land R \in LRing) \land m \in MaxIdeal (R)) \land \neg m \subseteq {Base}_{R} ∖ Unit (R)) \to \exists x \in m \neg x \in ({Base}_{R} ∖ Unit (R))$
26	23 25	r19.29a	$⊢ (((R \in CRing \land R \in LRing) \land m \in MaxIdeal (R)) \land \neg m \subseteq {Base}_{R} ∖ Unit (R)) \to m = {Base}_{R}$
27	2	ad2antrr	$⊢ (((R \in CRing \land R \in LRing) \land m \in MaxIdeal (R)) \land \neg m \subseteq {Base}_{R} ∖ Unit (R)) \to R \in Ring$
28		simplr	$⊢ (((R \in CRing \land R \in LRing) \land m \in MaxIdeal (R)) \land \neg m \subseteq {Base}_{R} ∖ Unit (R)) \to m \in MaxIdeal (R)$
29	5	mxidlnr	$⊢ (R \in Ring \land m \in MaxIdeal (R)) \to m \neq {Base}_{R}$
30	27 28 29	syl2anc	$⊢ (((R \in CRing \land R \in LRing) \land m \in MaxIdeal (R)) \land \neg m \subseteq {Base}_{R} ∖ Unit (R)) \to m \neq {Base}_{R}$
31	30	neneqd	$⊢ (((R \in CRing \land R \in LRing) \land m \in MaxIdeal (R)) \land \neg m \subseteq {Base}_{R} ∖ Unit (R)) \to \neg m = {Base}_{R}$
32	26 31	condan	$⊢ ((R \in CRing \land R \in LRing) \land m \in MaxIdeal (R)) \to m \subseteq {Base}_{R} ∖ Unit (R)$
33	5	mxidlmax	$⊢ ((R \in Ring \land m \in MaxIdeal (R)) \land ({Base}_{R} ∖ Unit (R) \in LIdeal (R) \land m \subseteq {Base}_{R} ∖ Unit (R))) \to ({Base}_{R} ∖ Unit (R) = m \lor {Base}_{R} ∖ Unit (R) = {Base}_{R})$
34	3 4 10 32 33	syl22anc	$⊢ ((R \in CRing \land R \in LRing) \land m \in MaxIdeal (R)) \to ({Base}_{R} ∖ Unit (R) = m \lor {Base}_{R} ∖ Unit (R) = {Base}_{R})$
35		eqid	$⊢ 1_{R} = 1_{R}$
36	5 35 1	ringidcld	$⊢ R \in CRing \to 1_{R} \in {Base}_{R}$
37	36	adantr	$⊢ (R \in CRing \land R \in LRing) \to 1_{R} \in {Base}_{R}$
38	6 35	1unit	$⊢ R \in Ring \to 1_{R} \in Unit (R)$
39		elndif	$⊢ 1_{R} \in Unit (R) \to \neg 1_{R} \in ({Base}_{R} ∖ Unit (R))$
40	2 38 39	3syl	$⊢ (R \in CRing \land R \in LRing) \to \neg 1_{R} \in ({Base}_{R} ∖ Unit (R))$
41		nelne1	$⊢ (1_{R} \in {Base}_{R} \land \neg 1_{R} \in ({Base}_{R} ∖ Unit (R))) \to {Base}_{R} \neq {Base}_{R} ∖ Unit (R)$
42	37 40 41	syl2anc	$⊢ (R \in CRing \land R \in LRing) \to {Base}_{R} \neq {Base}_{R} ∖ Unit (R)$
43	42	necomd	$⊢ (R \in CRing \land R \in LRing) \to {Base}_{R} ∖ Unit (R) \neq {Base}_{R}$
44	43	adantr	$⊢ ((R \in CRing \land R \in LRing) \land m \in MaxIdeal (R)) \to {Base}_{R} ∖ Unit (R) \neq {Base}_{R}$
45	44	neneqd	$⊢ ((R \in CRing \land R \in LRing) \land m \in MaxIdeal (R)) \to \neg {Base}_{R} ∖ Unit (R) = {Base}_{R}$
46	34 45	olcnd	$⊢ ((R \in CRing \land R \in LRing) \land m \in MaxIdeal (R)) \to {Base}_{R} ∖ Unit (R) = m$
47	46	eqcomd	$⊢ ((R \in CRing \land R \in LRing) \land m \in MaxIdeal (R)) \to m = {Base}_{R} ∖ Unit (R)$
48	5 6 7 8	dflringlem3	$⊢ (R \in CRing \land R \in LRing) \to {Base}_{R} ∖ Unit (R) \in MaxIdeal (R)$
49	47 48	eqsnd	$⊢ (R \in CRing \land R \in LRing) \to MaxIdeal (R) = \{{Base}_{R} ∖ Unit (R)\}$
50		ensn1g	$⊢ {Base}_{R} ∖ Unit (R) \in LIdeal (R) \to \{{Base}_{R} ∖ Unit (R)\} \approx 1_{𝑜}$
51	9 50	syl	$⊢ (R \in CRing \land R \in LRing) \to \{{Base}_{R} ∖ Unit (R)\} \approx 1_{𝑜}$
52	49 51	eqbrtrd	$⊢ (R \in CRing \land R \in LRing) \to MaxIdeal (R) \approx 1_{𝑜}$
53		en1	$⊢ MaxIdeal (R) \approx 1_{𝑜} \leftrightarrow \exists m MaxIdeal (R) = \{m\}$
54	53	bilani	$⊢ (R \in CRing \land MaxIdeal (R) \approx 1_{𝑜}) \to \exists m MaxIdeal (R) = \{m\}$
55	1	adantr	$⊢ (R \in CRing \land MaxIdeal (R) = \{m\}) \to R \in Ring$
56		vsnid	$⊢ m \in \{m\}$
57		simpr	$⊢ (R \in CRing \land MaxIdeal (R) = \{m\}) \to MaxIdeal (R) = \{m\}$
58	56 57	eleqtrrid	$⊢ (R \in CRing \land MaxIdeal (R) = \{m\}) \to m \in MaxIdeal (R)$
59	5	mxidlnzr	$⊢ (R \in Ring \land m \in MaxIdeal (R)) \to R \in NzRing$
60	55 58 59	syl2anc	$⊢ (R \in CRing \land MaxIdeal (R) = \{m\}) \to R \in NzRing$
61		simplll	$⊢ (((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land \neg x \in m) \to R \in CRing$
62	58	ad2antrr	$⊢ (((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land \neg x \in m) \to m \in MaxIdeal (R)$
63	57	ad2antrr	$⊢ (((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land \neg x \in m) \to MaxIdeal (R) = \{m\}$
64		simplr	$⊢ (((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land \neg x \in m) \to x \in {Base}_{R}$
65		simpr	$⊢ (((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land \neg x \in m) \to \neg x \in m$
66	64 65	eldifd	$⊢ (((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land \neg x \in m) \to x \in ({Base}_{R} ∖ m)$
67	5 6 61 62 63 66	dflringlem	$⊢ (((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land \neg x \in m) \to x \in Unit (R)$
68		simplll	$⊢ (((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land x \in m) \to R \in CRing$
69	58	ad2antrr	$⊢ (((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land x \in m) \to m \in MaxIdeal (R)$
70	57	ad2antrr	$⊢ (((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land x \in m) \to MaxIdeal (R) = \{m\}$
71		eqid	$⊢ -_{R} = -_{R}$
72	1	ringgrpd	$⊢ R \in CRing \to R \in Grp$
73	72	ad3antrrr	$⊢ (((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land x \in m) \to R \in Grp$
74	36	ad3antrrr	$⊢ (((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land x \in m) \to 1_{R} \in {Base}_{R}$
75		simplr	$⊢ (((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land x \in m) \to x \in {Base}_{R}$
76	5 71 73 74 75	grpsubcld	$⊢ (((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land x \in m) \to 1_{R} -_{R} x \in {Base}_{R}$
77	55	ad2antrr	$⊢ (((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land x \in m) \to R \in Ring$
78	5 35	mxidln1	$⊢ (R \in Ring \land m \in MaxIdeal (R)) \to \neg 1_{R} \in m$
79	77 69 78	syl2anc	$⊢ (((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land x \in m) \to \neg 1_{R} \in m$
80	73	adantr	$⊢ ((((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land x \in m) \land 1_{R} -_{R} x \in m) \to R \in Grp$
81	74	adantr	$⊢ ((((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land x \in m) \land 1_{R} -_{R} x \in m) \to 1_{R} \in {Base}_{R}$
82	75	adantr	$⊢ ((((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land x \in m) \land 1_{R} -_{R} x \in m) \to x \in {Base}_{R}$
83		eqid	$⊢ +_{R} = +_{R}$
84	5 83 71	grpnpcan	$⊢ (R \in Grp \land 1_{R} \in {Base}_{R} \land x \in {Base}_{R}) \to (1_{R} -_{R} x) +_{R} x = 1_{R}$
85	80 81 82 84	syl3anc	$⊢ ((((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land x \in m) \land 1_{R} -_{R} x \in m) \to (1_{R} -_{R} x) +_{R} x = 1_{R}$
86	77	adantr	$⊢ ((((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land x \in m) \land 1_{R} -_{R} x \in m) \to R \in Ring$
87	69	adantr	$⊢ ((((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land x \in m) \land 1_{R} -_{R} x \in m) \to m \in MaxIdeal (R)$
88	86 87 11	syl2anc	$⊢ ((((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land x \in m) \land 1_{R} -_{R} x \in m) \to m \in LIdeal (R)$
89		simpr	$⊢ ((((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land x \in m) \land 1_{R} -_{R} x \in m) \to 1_{R} -_{R} x \in m$
90		simplr	$⊢ ((((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land x \in m) \land 1_{R} -_{R} x \in m) \to x \in m$
91	13 83	lidlacl	$⊢ ((R \in Ring \land m \in LIdeal (R)) \land (1_{R} -_{R} x \in m \land x \in m)) \to (1_{R} -_{R} x) +_{R} x \in m$
92	86 88 89 90 91	syl22anc	$⊢ ((((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land x \in m) \land 1_{R} -_{R} x \in m) \to (1_{R} -_{R} x) +_{R} x \in m$
93	85 92	eqeltrrd	$⊢ ((((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land x \in m) \land 1_{R} -_{R} x \in m) \to 1_{R} \in m$
94	79 93	mtand	$⊢ (((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land x \in m) \to \neg 1_{R} -_{R} x \in m$
95	76 94	eldifd	$⊢ (((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land x \in m) \to 1_{R} -_{R} x \in ({Base}_{R} ∖ m)$
96	5 6 68 69 70 95	dflringlem	$⊢ (((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \land x \in m) \to 1_{R} -_{R} x \in Unit (R)$
97		exmidd	$⊢ ((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \to (x \in m \lor \neg x \in m)$
98	97	orcomd	$⊢ ((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \to (\neg x \in m \lor x \in m)$
99	67 96 98	orim12da	$⊢ ((R \in CRing \land MaxIdeal (R) = \{m\}) \land x \in {Base}_{R}) \to (x \in Unit (R) \lor 1_{R} -_{R} x \in Unit (R))$
100	99	ralrimiva	$⊢ (R \in CRing \land MaxIdeal (R) = \{m\}) \to \forall x \in {Base}_{R} (x \in Unit (R) \lor 1_{R} -_{R} x \in Unit (R))$
101	60 100	jca	$⊢ (R \in CRing \land MaxIdeal (R) = \{m\}) \to (R \in NzRing \land \forall x \in {Base}_{R} (x \in Unit (R) \lor 1_{R} -_{R} x \in Unit (R)))$
102	101	adantlr	$⊢ ((R \in CRing \land MaxIdeal (R) \approx 1_{𝑜}) \land MaxIdeal (R) = \{m\}) \to (R \in NzRing \land \forall x \in {Base}_{R} (x \in Unit (R) \lor 1_{R} -_{R} x \in Unit (R)))$
103	54 102	exlimddv	$⊢ (R \in CRing \land MaxIdeal (R) \approx 1_{𝑜}) \to (R \in NzRing \land \forall x \in {Base}_{R} (x \in Unit (R) \lor 1_{R} -_{R} x \in Unit (R)))$
104	5 6 35 71	dflring2	$⊢ R \in LRing \leftrightarrow (R \in NzRing \land \forall x \in {Base}_{R} (x \in Unit (R) \lor 1_{R} -_{R} x \in Unit (R)))$
105	103 104	sylibr	$⊢ (R \in CRing \land MaxIdeal (R) \approx 1_{𝑜}) \to R \in LRing$
106	52 105	impbida	$⊢ R \in CRing \to (R \in LRing \leftrightarrow MaxIdeal (R) \approx 1_{𝑜})$

Metamath Proof Explorer

Theorem dflring3

Proof