dflringlem3

Description: Lemma for dflring3 . In a commutative local ring R , the set ( B \ U ) of non-units is a maximal ideal. (Contributed by Thierry Arnoux, 2-Jun-2026)

	Ref	Expression
Hypotheses	dflringlem2.b	$⊢ B = {Base}_{R}$
	dflringlem2.u	$⊢ U = Unit (R)$
	dflringlem2.1	$⊢ φ \to R \in CRing$
	dflringlem2.2	$⊢ φ \to R \in LRing$
Assertion	dflringlem3	$⊢ φ \to B ∖ U \in MaxIdeal (R)$

Proof

Step	Hyp	Ref	Expression
1		dflringlem2.b	$⊢ B = {Base}_{R}$
2		dflringlem2.u	$⊢ U = Unit (R)$
3		dflringlem2.1	$⊢ φ \to R \in CRing$
4		dflringlem2.2	$⊢ φ \to R \in LRing$
5		crngring	$⊢ R \in CRing \to R \in Ring$
6	3 5	syl	$⊢ φ \to R \in Ring$
7	1 2 3 4	dflringlem2	$⊢ φ \to B ∖ U \in LIdeal (R)$
8		eqid	$⊢ 1_{R} = 1_{R}$
9	1 8 5	ringidcld	$⊢ R \in CRing \to 1_{R} \in B$
10	3 9	syl	$⊢ φ \to 1_{R} \in B$
11	2 8	1unit	$⊢ R \in Ring \to 1_{R} \in U$
12	6 11	syl	$⊢ φ \to 1_{R} \in U$
13		elndif	$⊢ 1_{R} \in U \to \neg 1_{R} \in (B ∖ U)$
14	12 13	syl	$⊢ φ \to \neg 1_{R} \in (B ∖ U)$
15		nelne1	$⊢ (1_{R} \in B \land \neg 1_{R} \in (B ∖ U)) \to B \neq B ∖ U$
16	10 14 15	syl2anc	$⊢ φ \to B \neq B ∖ U$
17	16	necomd	$⊢ φ \to B ∖ U \neq B$
18		eqid	$⊢ LIdeal (R) = LIdeal (R)$
19	1 18	lidlss	$⊢ j \in LIdeal (R) \to j \subseteq B$
20	19	ad3antlr	$⊢ (((φ \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \land \neg j = B ∖ U) \to j \subseteq B$
21		ssdif0	$⊢ j \subseteq B \leftrightarrow j ∖ B = \emptyset$
22	20 21	sylib	$⊢ (((φ \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \land \neg j = B ∖ U) \to j ∖ B = \emptyset$
23	22	uneq1d	$⊢ (((φ \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)$
24		0un	$⊢ \emptyset \cup (j \cap U) = j \cap U$
25	23 24	eqtr2di	$⊢ (((φ \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)$
26		simplr	$⊢ (((φ \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \land \neg j = B ∖ U) \to B ∖ U \subseteq j$
27		neqne	$⊢ \neg j = B ∖ U \to j \neq B ∖ U$
28	27	adantl	$⊢ (((φ \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \land \neg j = B ∖ U) \to j \neq B ∖ U$
29	28	necomd	$⊢ (((φ \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \land \neg j = B ∖ U) \to B ∖ U \neq j$
30		difdif2	$⊢ j ∖ (B ∖ U) = (j ∖ B) \cup (j \cap U)$
31		pssdifn0	$⊢ (B ∖ U \subseteq j \land B ∖ U \neq j) \to j ∖ (B ∖ U) \neq \emptyset$
32	30 31	eqnetrrid	$⊢ (B ∖ U \subseteq j \land B ∖ U \neq j) \to (j ∖ B) \cup (j \cap U) \neq \emptyset$
33	26 29 32	syl2anc	$⊢ (((φ \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \land \neg j = B ∖ U) \to (j ∖ B) \cup (j \cap U) \neq \emptyset$
34	25 33	eqnetrd	$⊢ (((φ \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \land \neg j = B ∖ U) \to j \cap U \neq \emptyset$
35		simpr	$⊢ ((((φ \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)$
36	35	elin2d	$⊢ ((((φ \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$
37	35	elin1d	$⊢ ((((φ \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$
38	6	ad4antr	$⊢ ((((φ \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$
39		simp-4r	$⊢ ((((φ \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)$
40	1 2 36 37 38 39	lidlunitel	$⊢ ((((φ \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \land \neg j = B ∖ U) \land x \in (j \cap U)) \to j = B$
41	34 40	n0limd	$⊢ (((φ \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \land \neg j = B ∖ U) \to j = B$
42	41	ex	$⊢ ((φ \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \to (\neg j = B ∖ U \to j = B)$
43	42	orrd	$⊢ ((φ \land j \in LIdeal (R)) \land B ∖ U \subseteq j) \to (j = B ∖ U \lor j = B)$
44	43	ex	$⊢ (φ \land j \in LIdeal (R)) \to (B ∖ U \subseteq j \to (j = B ∖ U \lor j = B))$
45	44	ralrimiva	$⊢ φ \to \forall j \in LIdeal (R) (B ∖ U \subseteq j \to (j = B ∖ U \lor j = B))$
46	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))))$
47	46	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)$
48	6 7 17 45 47	syl13anc	$⊢ φ \to B ∖ U \in MaxIdeal (R)$

Metamath Proof Explorer

Theorem dflringlem3

Proof