dflring4

Description: Alternate definition of a local ring: the set ( B \ U ) of non-units is an ideal. (Contributed by Thierry Arnoux, 2-Jun-2026)

	Ref	Expression
Hypotheses	dflring4.b	$⊢ B = {Base}_{R}$
	dflring4.u	$⊢ U = Unit (R)$
Assertion	dflring4	$⊢ R \in CRing \to (R \in LRing \leftrightarrow B ∖ U \in LIdeal (R))$

Proof

Step	Hyp	Ref	Expression
1		dflring4.b	$⊢ B = {Base}_{R}$
2		dflring4.u	$⊢ U = Unit (R)$
3		simpl	$⊢ (R \in CRing \land R \in LRing) \to R \in CRing$
4		simpr	$⊢ (R \in CRing \land R \in LRing) \to R \in LRing$
5	1 2 3 4	dflringlem2	$⊢ (R \in CRing \land R \in LRing) \to B ∖ U \in LIdeal (R)$
6		simpl	$⊢ (R \in CRing \land B ∖ U \in LIdeal (R)) \to R \in CRing$
7	6	crngringd	$⊢ (R \in CRing \land B ∖ U \in LIdeal (R)) \to R \in Ring$
8	7	adantr	$⊢ ((R \in CRing \land B ∖ U \in LIdeal (R)) \land m \in MaxIdeal (R)) \to R \in Ring$
9		simpr	$⊢ ((R \in CRing \land B ∖ U \in LIdeal (R)) \land m \in MaxIdeal (R)) \to m \in MaxIdeal (R)$
10		simplr	$⊢ ((R \in CRing \land B ∖ U \in LIdeal (R)) \land m \in MaxIdeal (R)) \to B ∖ U \in LIdeal (R)$
11	1	mxidlidl	$⊢ (R \in Ring \land m \in MaxIdeal (R)) \to m \in LIdeal (R)$
12	7 11	sylan	$⊢ ((R \in CRing \land B ∖ U \in LIdeal (R)) \land m \in MaxIdeal (R)) \to m \in LIdeal (R)$
13		eqid	$⊢ LIdeal (R) = LIdeal (R)$
14	1 13	lidlss	$⊢ m \in LIdeal (R) \to m \subseteq B$
15	12 14	syl	$⊢ ((R \in CRing \land B ∖ U \in LIdeal (R)) \land m \in MaxIdeal (R)) \to m \subseteq B$
16	15	adantr	$⊢ (((R \in CRing \land B ∖ U \in LIdeal (R)) \land m \in MaxIdeal (R)) \land \neg m \subseteq B ∖ U) \to m \subseteq B$
17	16	sselda	$⊢ ((((R \in CRing \land B ∖ U \in LIdeal (R)) \land m \in MaxIdeal (R)) \land \neg m \subseteq B ∖ U) \land x \in m) \to x \in B$
18		neldif	$⊢ (x \in B \land \neg x \in (B ∖ U)) \to x \in U$
19	17 18	sylan	$⊢ (((((R \in CRing \land B ∖ U \in LIdeal (R)) \land m \in MaxIdeal (R)) \land \neg m \subseteq B ∖ U) \land x \in m) \land \neg x \in (B ∖ U)) \to x \in U$
20		simplr	$⊢ (((((R \in CRing \land B ∖ U \in LIdeal (R)) \land m \in MaxIdeal (R)) \land \neg m \subseteq B ∖ U) \land x \in m) \land \neg x \in (B ∖ U)) \to x \in m$
21	8	ad3antrrr	$⊢ (((((R \in CRing \land B ∖ U \in LIdeal (R)) \land m \in MaxIdeal (R)) \land \neg m \subseteq B ∖ U) \land x \in m) \land \neg x \in (B ∖ U)) \to R \in Ring$
22	12	ad3antrrr	$⊢ (((((R \in CRing \land B ∖ U \in LIdeal (R)) \land m \in MaxIdeal (R)) \land \neg m \subseteq B ∖ U) \land x \in m) \land \neg x \in (B ∖ U)) \to m \in LIdeal (R)$
23	1 2 19 20 21 22	lidlunitel	$⊢ (((((R \in CRing \land B ∖ U \in LIdeal (R)) \land m \in MaxIdeal (R)) \land \neg m \subseteq B ∖ U) \land x \in m) \land \neg x \in (B ∖ U)) \to m = B$
24		nssrex	$⊢ \neg m \subseteq B ∖ U \leftrightarrow \exists x \in m \neg x \in (B ∖ U)$
25	24	bilani	$⊢ (((R \in CRing \land B ∖ U \in LIdeal (R)) \land m \in MaxIdeal (R)) \land \neg m \subseteq B ∖ U) \to \exists x \in m \neg x \in (B ∖ U)$
26	23 25	r19.29a	$⊢ (((R \in CRing \land B ∖ U \in LIdeal (R)) \land m \in MaxIdeal (R)) \land \neg m \subseteq B ∖ U) \to m = B$
27	8	adantr	$⊢ (((R \in CRing \land B ∖ U \in LIdeal (R)) \land m \in MaxIdeal (R)) \land \neg m \subseteq B ∖ U) \to R \in Ring$
28		simplr	$⊢ (((R \in CRing \land B ∖ U \in LIdeal (R)) \land m \in MaxIdeal (R)) \land \neg m \subseteq B ∖ U) \to m \in MaxIdeal (R)$
29	1	mxidlnr	$⊢ (R \in Ring \land m \in MaxIdeal (R)) \to m \neq B$
30	27 28 29	syl2anc	$⊢ (((R \in CRing \land B ∖ U \in LIdeal (R)) \land m \in MaxIdeal (R)) \land \neg m \subseteq B ∖ U) \to m \neq B$
31	30	neneqd	$⊢ (((R \in CRing \land B ∖ U \in LIdeal (R)) \land m \in MaxIdeal (R)) \land \neg m \subseteq B ∖ U) \to \neg m = B$
32	26 31	condan	$⊢ ((R \in CRing \land B ∖ U \in LIdeal (R)) \land m \in MaxIdeal (R)) \to m \subseteq B ∖ U$
33	1	mxidlmax	$⊢ ((R \in Ring \land m \in MaxIdeal (R)) \land (B ∖ U \in LIdeal (R) \land m \subseteq B ∖ U)) \to (B ∖ U = m \lor B ∖ U = B)$
34	8 9 10 32 33	syl22anc	$⊢ ((R \in CRing \land B ∖ U \in LIdeal (R)) \land m \in MaxIdeal (R)) \to (B ∖ U = m \lor B ∖ U = B)$
35		eqid	$⊢ 1_{R} = 1_{R}$
36	1 35 7	ringidcld	$⊢ (R \in CRing \land B ∖ U \in LIdeal (R)) \to 1_{R} \in B$
37	2 35	1unit	$⊢ R \in Ring \to 1_{R} \in U$
38	7 37	syl	$⊢ (R \in CRing \land B ∖ U \in LIdeal (R)) \to 1_{R} \in U$
39		elndif	$⊢ 1_{R} \in U \to \neg 1_{R} \in (B ∖ U)$
40	38 39	syl	$⊢ (R \in CRing \land B ∖ U \in LIdeal (R)) \to \neg 1_{R} \in (B ∖ U)$
41		nelne1	$⊢ (1_{R} \in B \land \neg 1_{R} \in (B ∖ U)) \to B \neq B ∖ U$
42	36 40 41	syl2anc	$⊢ (R \in CRing \land B ∖ U \in LIdeal (R)) \to B \neq B ∖ U$
43	42	necomd	$⊢ (R \in CRing \land B ∖ U \in LIdeal (R)) \to B ∖ U \neq B$
44	43	adantr	$⊢ ((R \in CRing \land B ∖ U \in LIdeal (R)) \land m \in MaxIdeal (R)) \to B ∖ U \neq B$
45	44	neneqd	$⊢ ((R \in CRing \land B ∖ U \in LIdeal (R)) \land m \in MaxIdeal (R)) \to \neg B ∖ U = B$
46	34 45	olcnd	$⊢ ((R \in CRing \land B ∖ U \in LIdeal (R)) \land m \in MaxIdeal (R)) \to B ∖ U = m$
47	46	eqcomd	$⊢ ((R \in CRing \land B ∖ U \in LIdeal (R)) \land m \in MaxIdeal (R)) \to m = B ∖ U$
48		simpr	$⊢ (R \in CRing \land B ∖ U \in LIdeal (R)) \to B ∖ U \in LIdeal (R)$
49	1 13	lidlss	$⊢ j \in LIdeal (R) \to j \subseteq B$
50	49	ad3antlr	$⊢ ((((R \in CRing \land B ∖ U \in LIdeal (R)) \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \land \neg j = B ∖ U) \to j \subseteq B$
51		ssdif0	$⊢ j \subseteq B \leftrightarrow j ∖ B = \emptyset$
52	50 51	sylib	$⊢ ((((R \in CRing \land B ∖ U \in LIdeal (R)) \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \land \neg j = B ∖ U) \to j ∖ B = \emptyset$
53	52	uneq1d	$⊢ ((((R \in CRing \land B ∖ U \in LIdeal (R)) \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \land \neg j = B ∖ U) \to (j ∖ B) \cup (j \cap U) = \emptyset \cup (j \cap U)$
54		0un	$⊢ \emptyset \cup (j \cap U) = j \cap U$
55	53 54	eqtr2di	$⊢ ((((R \in CRing \land B ∖ U \in LIdeal (R)) \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \land \neg j = B ∖ U) \to j \cap U = (j ∖ B) \cup (j \cap U)$
56		simplr	$⊢ ((((R \in CRing \land B ∖ U \in LIdeal (R)) \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \land \neg j = B ∖ U) \to B ∖ U \subseteq j$
57		neqne	$⊢ \neg j = B ∖ U \to j \neq B ∖ U$
58	57	adantl	$⊢ ((((R \in CRing \land B ∖ U \in LIdeal (R)) \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \land \neg j = B ∖ U) \to j \neq B ∖ U$
59	58	necomd	$⊢ ((((R \in CRing \land B ∖ U \in LIdeal (R)) \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \land \neg j = B ∖ U) \to B ∖ U \neq j$
60		difdif2	$⊢ j ∖ (B ∖ U) = (j ∖ B) \cup (j \cap U)$
61		pssdifn0	$⊢ (B ∖ U \subseteq j \land B ∖ U \neq j) \to j ∖ (B ∖ U) \neq \emptyset$
62	60 61	eqnetrrid	$⊢ (B ∖ U \subseteq j \land B ∖ U \neq j) \to (j ∖ B) \cup (j \cap U) \neq \emptyset$
63	56 59 62	syl2anc	$⊢ ((((R \in CRing \land B ∖ U \in LIdeal (R)) \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \land \neg j = B ∖ U) \to (j ∖ B) \cup (j \cap U) \neq \emptyset$
64	55 63	eqnetrd	$⊢ ((((R \in CRing \land B ∖ U \in LIdeal (R)) \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \land \neg j = B ∖ U) \to j \cap U \neq \emptyset$
65		simpr	$⊢ (((((R \in CRing \land B ∖ U \in LIdeal (R)) \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \land \neg j = B ∖ U) \land x \in (j \cap U)) \to x \in (j \cap U)$
66	65	elin2d	$⊢ (((((R \in CRing \land B ∖ U \in LIdeal (R)) \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \land \neg j = B ∖ U) \land x \in (j \cap U)) \to x \in U$
67	65	elin1d	$⊢ (((((R \in CRing \land B ∖ U \in LIdeal (R)) \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \land \neg j = B ∖ U) \land x \in (j \cap U)) \to x \in j$
68	7	ad4antr	$⊢ (((((R \in CRing \land B ∖ U \in LIdeal (R)) \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \land \neg j = B ∖ U) \land x \in (j \cap U)) \to R \in Ring$
69		simp-4r	$⊢ (((((R \in CRing \land B ∖ U \in LIdeal (R)) \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \land \neg j = B ∖ U) \land x \in (j \cap U)) \to j \in LIdeal (R)$
70	1 2 66 67 68 69	lidlunitel	$⊢ (((((R \in CRing \land B ∖ U \in LIdeal (R)) \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \land \neg j = B ∖ U) \land x \in (j \cap U)) \to j = B$
71	64 70	n0limd	$⊢ ((((R \in CRing \land B ∖ U \in LIdeal (R)) \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \land \neg j = B ∖ U) \to j = B$
72	71	ex	$⊢ (((R \in CRing \land B ∖ U \in LIdeal (R)) \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \to (\neg j = B ∖ U \to j = B)$
73	72	orrd	$⊢ (((R \in CRing \land B ∖ U \in LIdeal (R)) \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \to (j = B ∖ U \lor j = B)$
74	73	ex	$⊢ ((R \in CRing \land B ∖ U \in LIdeal (R)) \land j \in LIdeal (R)) \to (B ∖ U \subseteq j \to (j = B ∖ U \lor j = B))$
75	74	ralrimiva	$⊢ (R \in CRing \land B ∖ U \in LIdeal (R)) \to \forall j \in LIdeal (R) (B ∖ U \subseteq j \to (j = B ∖ U \lor j = B))$
76	1	ismxidl	$⊢ R \in Ring \to (B ∖ U \in MaxIdeal (R) \leftrightarrow (B ∖ U \in LIdeal (R) \land B ∖ U \neq B \land \forall j \in LIdeal (R) (B ∖ U \subseteq j \to (j = B ∖ U \lor j = B))))$
77	76	biimpar	$⊢ (R \in Ring \land (B ∖ U \in LIdeal (R) \land B ∖ U \neq B \land \forall j \in LIdeal (R) (B ∖ U \subseteq j \to (j = B ∖ U \lor j = B)))) \to B ∖ U \in MaxIdeal (R)$
78	7 48 43 75 77	syl13anc	$⊢ (R \in CRing \land B ∖ U \in LIdeal (R)) \to B ∖ U \in MaxIdeal (R)$
79	47 78	eqsnd	$⊢ (R \in CRing \land B ∖ U \in LIdeal (R)) \to MaxIdeal (R) = \{B ∖ U\}$
80	1	fvexi	$⊢ B \in V$
81	80	a1i	$⊢ (R \in CRing \land B ∖ U \in LIdeal (R)) \to B \in V$
82	81	difexd	$⊢ (R \in CRing \land B ∖ U \in LIdeal (R)) \to B ∖ U \in V$
83		ensn1g	$⊢ B ∖ U \in V \to \{B ∖ U\} \approx 1_{𝑜}$
84	82 83	syl	$⊢ (R \in CRing \land B ∖ U \in LIdeal (R)) \to \{B ∖ U\} \approx 1_{𝑜}$
85	79 84	eqbrtrd	$⊢ (R \in CRing \land B ∖ U \in LIdeal (R)) \to MaxIdeal (R) \approx 1_{𝑜}$
86		dflring3	$⊢ R \in CRing \to (R \in LRing \leftrightarrow MaxIdeal (R) \approx 1_{𝑜})$
87	86	biimpar	$⊢ (R \in CRing \land MaxIdeal (R) \approx 1_{𝑜}) \to R \in LRing$
88	6 85 87	syl2anc	$⊢ (R \in CRing \land B ∖ U \in LIdeal (R)) \to R \in LRing$
89	5 88	impbida	$⊢ R \in CRing \to (R \in LRing \leftrightarrow B ∖ U \in LIdeal (R))$

Metamath Proof Explorer

Theorem dflring4

Proof