dflringlem2

Description: Lemma for dflring3 . In a commutative local ring R , the set ( B \ U ) of non-units is an 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	dflringlem2	$⊢ φ \to B ∖ U \in LIdeal (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		difssd	$⊢ φ \to B ∖ U \subseteq B$
6		eqid	$⊢ 0_{R} = 0_{R}$
7	3	crnggrpd	$⊢ φ \to R \in Grp$
8	1 6 7	grpidcld	$⊢ φ \to 0_{R} \in B$
9		lringnzr	$⊢ R \in LRing \to R \in NzRing$
10	4 9	syl	$⊢ φ \to R \in NzRing$
11	10	adantr	$⊢ (φ \land x \in U) \to R \in NzRing$
12		simpr	$⊢ (φ \land x \in U) \to x \in U$
13	2 6 11 12	unitnz	$⊢ (φ \land x \in U) \to x \neq 0_{R}$
14	13	nelrdva	$⊢ φ \to \neg 0_{R} \in U$
15	8 14	eldifd	$⊢ φ \to 0_{R} \in (B ∖ U)$
16	15	ne0d	$⊢ φ \to B ∖ U \neq \emptyset$
17		eqid	$⊢ +_{R} = +_{R}$
18	7	ad3antrrr	$⊢ (((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \to R \in Grp$
19		eqid	$⊢ \cdot_{R} = \cdot_{R}$
20	3	crngringd	$⊢ φ \to R \in Ring$
21	20	ad3antrrr	$⊢ (((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \to R \in Ring$
22		simpllr	$⊢ (((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \to x \in B$
23		simplr	$⊢ (((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \to a \in (B ∖ U)$
24	23	eldifad	$⊢ (((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \to a \in B$
25	1 19 21 22 24	ringcld	$⊢ (((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \to x \cdot_{R} a \in B$
26		simpr	$⊢ (((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \to b \in (B ∖ U)$
27	26	eldifad	$⊢ (((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \to b \in B$
28	1 17 18 25 27	grpcld	$⊢ (((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \to (x \cdot_{R} a) +_{R} b \in B$
29	23	eldifbd	$⊢ (((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \to \neg a \in U$
30	26	eldifbd	$⊢ (((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \to \neg b \in U$
31		ioran	$⊢ \neg (a \in U \lor b \in U) \leftrightarrow (\neg a \in U \land \neg b \in U)$
32	29 30 31	sylanbrc	$⊢ (((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \to \neg (a \in U \lor b \in U)$
33	3	ad6antr	$⊢ ((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \to R \in CRing$
34	33	adantr	$⊢ (((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \land (x \cdot_{R} a) \cdot_{R} u \in U) \to R \in CRing$
35	22	ad4antr	$⊢ (((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \land (x \cdot_{R} a) \cdot_{R} u \in U) \to x \in B$
36	24	ad4antr	$⊢ (((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \land (x \cdot_{R} a) \cdot_{R} u \in U) \to a \in B$
37	25	ad3antrrr	$⊢ ((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \to x \cdot_{R} a \in B$
38	37	adantr	$⊢ (((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \land (x \cdot_{R} a) \cdot_{R} u \in U) \to x \cdot_{R} a \in B$
39		simplr	$⊢ ((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \to u \in B$
40	39	adantr	$⊢ (((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \land (x \cdot_{R} a) \cdot_{R} u \in U) \to u \in B$
41		simpr	$⊢ (((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \land (x \cdot_{R} a) \cdot_{R} u \in U) \to (x \cdot_{R} a) \cdot_{R} u \in U$
42	2 19 1	unitmulclb	$⊢ (R \in CRing \land x \cdot_{R} a \in B \land u \in B) \to ((x \cdot_{R} a) \cdot_{R} u \in U \leftrightarrow (x \cdot_{R} a \in U \land u \in U))$
43	42	simprbda	$⊢ ((R \in CRing \land x \cdot_{R} a \in B \land u \in B) \land (x \cdot_{R} a) \cdot_{R} u \in U) \to x \cdot_{R} a \in U$
44	34 38 40 41 43	syl31anc	$⊢ (((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \land (x \cdot_{R} a) \cdot_{R} u \in U) \to x \cdot_{R} a \in U$
45	2 19 1	unitmulclb	$⊢ (R \in CRing \land x \in B \land a \in B) \to (x \cdot_{R} a \in U \leftrightarrow (x \in U \land a \in U))$
46	45	simplbda	$⊢ ((R \in CRing \land x \in B \land a \in B) \land x \cdot_{R} a \in U) \to a \in U$
47	34 35 36 44 46	syl31anc	$⊢ (((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \land (x \cdot_{R} a) \cdot_{R} u \in U) \to a \in U$
48	33	adantr	$⊢ (((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \land b \cdot_{R} u \in U) \to R \in CRing$
49	27	ad3antrrr	$⊢ ((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \to b \in B$
50	49	adantr	$⊢ (((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \land b \cdot_{R} u \in U) \to b \in B$
51	39	adantr	$⊢ (((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \land b \cdot_{R} u \in U) \to u \in B$
52		simpr	$⊢ (((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \land b \cdot_{R} u \in U) \to b \cdot_{R} u \in U$
53	2 19 1	unitmulclb	$⊢ (R \in CRing \land b \in B \land u \in B) \to (b \cdot_{R} u \in U \leftrightarrow (b \in U \land u \in U))$
54	53	simprbda	$⊢ ((R \in CRing \land b \in B \land u \in B) \land b \cdot_{R} u \in U) \to b \in U$
55	48 50 51 52 54	syl31anc	$⊢ (((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \land b \cdot_{R} u \in U) \to b \in U$
56	1	a1i	$⊢ ((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \to B = {Base}_{R}$
57	2	a1i	$⊢ ((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \to U = Unit (R)$
58	17	a1i	$⊢ ((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \to +_{R} = +_{R}$
59	4	ad6antr	$⊢ ((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \to R \in LRing$
60	21	ad3antrrr	$⊢ ((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \to R \in Ring$
61	1 17 19 60 37 49 39	ringdird	$⊢ ((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \to ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = ((x \cdot_{R} a) \cdot_{R} u) +_{R} (b \cdot_{R} u)$
62		simpr	$⊢ ((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \to ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}$
63	61 62	eqtr3d	$⊢ ((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \to ((x \cdot_{R} a) \cdot_{R} u) +_{R} (b \cdot_{R} u) = 1_{R}$
64		eqid	$⊢ 1_{R} = 1_{R}$
65	2 64	1unit	$⊢ R \in Ring \to 1_{R} \in U$
66	20 65	syl	$⊢ φ \to 1_{R} \in U$
67	66	ad6antr	$⊢ ((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \to 1_{R} \in U$
68	63 67	eqeltrd	$⊢ ((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \to ((x \cdot_{R} a) \cdot_{R} u) +_{R} (b \cdot_{R} u) \in U$
69	1 19 60 37 39	ringcld	$⊢ ((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \to (x \cdot_{R} a) \cdot_{R} u \in B$
70	1 19 60 49 39	ringcld	$⊢ ((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \to b \cdot_{R} u \in B$
71	56 57 58 59 68 69 70	lringuplu	$⊢ ((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \to ((x \cdot_{R} a) \cdot_{R} u \in U \lor b \cdot_{R} u \in U)$
72	47 55 71	orim12da	$⊢ ((((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \land u \in B) \land ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}) \to (a \in U \lor b \in U)$
73	1 2 19 64 28 21	isunit3	$⊢ (((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \to ((x \cdot_{R} a) +_{R} b \in U \leftrightarrow \exists u \in B (((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R} \land u \cdot_{R} ((x \cdot_{R} a) +_{R} b) = 1_{R}))$
74	73	biimpa	$⊢ ((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \to \exists u \in B (((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R} \land u \cdot_{R} ((x \cdot_{R} a) +_{R} b) = 1_{R})$
75		simpl	$⊢ (((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R} \land u \cdot_{R} ((x \cdot_{R} a) +_{R} b) = 1_{R}) \to ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}$
76	75	reximi	$⊢ \exists u \in B (((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R} \land u \cdot_{R} ((x \cdot_{R} a) +_{R} b) = 1_{R}) \to \exists u \in B ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}$
77	74 76	syl	$⊢ ((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \to \exists u \in B ((x \cdot_{R} a) +_{R} b) \cdot_{R} u = 1_{R}$
78	72 77	r19.29a	$⊢ ((((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \land (x \cdot_{R} a) +_{R} b \in U) \to (a \in U \lor b \in U)$
79	32 78	mtand	$⊢ (((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \to \neg (x \cdot_{R} a) +_{R} b \in U$
80	28 79	eldifd	$⊢ (((φ \land x \in B) \land a \in (B ∖ U)) \land b \in (B ∖ U)) \to (x \cdot_{R} a) +_{R} b \in (B ∖ U)$
81	80	ralrimiva	$⊢ ((φ \land x \in B) \land a \in (B ∖ U)) \to \forall b \in (B ∖ U) (x \cdot_{R} a) +_{R} b \in (B ∖ U)$
82	81	anasss	$⊢ (φ \land (x \in B \land a \in (B ∖ U))) \to \forall b \in (B ∖ U) (x \cdot_{R} a) +_{R} b \in (B ∖ U)$
83	82	ralrimivva	$⊢ φ \to \forall x \in B \forall a \in (B ∖ U) \forall b \in (B ∖ U) (x \cdot_{R} a) +_{R} b \in (B ∖ U)$
84		eqid	$⊢ LIdeal (R) = LIdeal (R)$
85	84 1 17 19	islidl	$⊢ B ∖ U \in LIdeal (R) \leftrightarrow (B ∖ U \subseteq B \land B ∖ U \neq \emptyset \land \forall x \in B \forall a \in (B ∖ U) \forall b \in (B ∖ U) (x \cdot_{R} a) +_{R} b \in (B ∖ U))$
86	5 16 83 85	syl3anbrc	$⊢ φ \to B ∖ U \in LIdeal (R)$

Metamath Proof Explorer

Theorem dflringlem2

Proof