dflring2

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

	Ref	Expression
Hypotheses	dflring2.1	$⊢ B = {Base}_{R}$
	dflring2.2	$⊢ U = Unit (R)$
	dflring2.3	$⊢ \underset{˙}{1} = 1_{R}$
	dflring2.4	$⊢ \underset{˙}{-} = -_{R}$
Assertion	dflring2	$⊢ R \in LRing \leftrightarrow (R \in NzRing \land \forall x \in B (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U))$

Proof

Step	Hyp	Ref	Expression
1		dflring2.1	$⊢ B = {Base}_{R}$
2		dflring2.2	$⊢ U = Unit (R)$
3		dflring2.3	$⊢ \underset{˙}{1} = 1_{R}$
4		dflring2.4	$⊢ \underset{˙}{-} = -_{R}$
5		lringnzr	$⊢ R \in LRing \to R \in NzRing$
6	1	a1i	$⊢ (R \in LRing \land x \in B) \to B = {Base}_{R}$
7	2	a1i	$⊢ (R \in LRing \land x \in B) \to U = Unit (R)$
8		eqidd	$⊢ (R \in LRing \land x \in B) \to +_{R} = +_{R}$
9		simpl	$⊢ (R \in LRing \land x \in B) \to R \in LRing$
10		lringring	$⊢ R \in LRing \to R \in Ring$
11	10	ringabld	$⊢ R \in LRing \to R \in Abel$
12	11	adantr	$⊢ (R \in LRing \land x \in B) \to R \in Abel$
13		simpr	$⊢ (R \in LRing \land x \in B) \to x \in B$
14	1 3 10	ringidcld	$⊢ R \in LRing \to \underset{˙}{1} \in B$
15	14	adantr	$⊢ (R \in LRing \land x \in B) \to \underset{˙}{1} \in B$
16		eqid	$⊢ +_{R} = +_{R}$
17	1 16 4	ablpncan3	$⊢ (R \in Abel \land (x \in B \land \underset{˙}{1} \in B)) \to x +_{R} (\underset{˙}{1} \underset{˙}{-} x) = \underset{˙}{1}$
18	12 13 15 17	syl12anc	$⊢ (R \in LRing \land x \in B) \to x +_{R} (\underset{˙}{1} \underset{˙}{-} x) = \underset{˙}{1}$
19	2 3	1unit	$⊢ R \in Ring \to \underset{˙}{1} \in U$
20	10 19	syl	$⊢ R \in LRing \to \underset{˙}{1} \in U$
21	20	adantr	$⊢ (R \in LRing \land x \in B) \to \underset{˙}{1} \in U$
22	18 21	eqeltrd	$⊢ (R \in LRing \land x \in B) \to x +_{R} (\underset{˙}{1} \underset{˙}{-} x) \in U$
23	10	ringgrpd	$⊢ R \in LRing \to R \in Grp$
24	23	adantr	$⊢ (R \in LRing \land x \in B) \to R \in Grp$
25	1 4 24 15 13	grpsubcld	$⊢ (R \in LRing \land x \in B) \to \underset{˙}{1} \underset{˙}{-} x \in B$
26	6 7 8 9 22 13 25	lringuplu	$⊢ (R \in LRing \land x \in B) \to (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U)$
27	26	ralrimiva	$⊢ R \in LRing \to \forall x \in B (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U)$
28	5 27	jca	$⊢ R \in LRing \to (R \in NzRing \land \forall x \in B (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U))$
29		simpl	$⊢ (R \in NzRing \land \forall x \in B (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U)) \to R \in NzRing$
30		simpr	$⊢ (((((R \in NzRing \land x \in B) \land (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U)) \land y \in B) \land x +_{R} y = \underset{˙}{1}) \land x \in U) \to x \in U$
31		nzrring	$⊢ R \in NzRing \to R \in Ring$
32	31	ringgrpd	$⊢ R \in NzRing \to R \in Grp$
33	32	ad4antr	$⊢ ((((R \in NzRing \land x \in B) \land (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U)) \land y \in B) \land x +_{R} y = \underset{˙}{1}) \to R \in Grp$
34	1 3 31	ringidcld	$⊢ R \in NzRing \to \underset{˙}{1} \in B$
35	34	ad4antr	$⊢ ((((R \in NzRing \land x \in B) \land (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U)) \land y \in B) \land x +_{R} y = \underset{˙}{1}) \to \underset{˙}{1} \in B$
36		simp-4r	$⊢ ((((R \in NzRing \land x \in B) \land (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U)) \land y \in B) \land x +_{R} y = \underset{˙}{1}) \to x \in B$
37		simplr	$⊢ ((((R \in NzRing \land x \in B) \land (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U)) \land y \in B) \land x +_{R} y = \underset{˙}{1}) \to y \in B$
38	35 36 37	3jca	$⊢ ((((R \in NzRing \land x \in B) \land (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U)) \land y \in B) \land x +_{R} y = \underset{˙}{1}) \to (\underset{˙}{1} \in B \land x \in B \land y \in B)$
39	31	ringabld	$⊢ R \in NzRing \to R \in Abel$
40	39	ad4antr	$⊢ ((((R \in NzRing \land x \in B) \land (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U)) \land y \in B) \land x +_{R} y = \underset{˙}{1}) \to R \in Abel$
41	1 16 40 37 36	ablcomd	$⊢ ((((R \in NzRing \land x \in B) \land (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U)) \land y \in B) \land x +_{R} y = \underset{˙}{1}) \to y +_{R} x = x +_{R} y$
42		simpr	$⊢ ((((R \in NzRing \land x \in B) \land (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U)) \land y \in B) \land x +_{R} y = \underset{˙}{1}) \to x +_{R} y = \underset{˙}{1}$
43	41 42	eqtrd	$⊢ ((((R \in NzRing \land x \in B) \land (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U)) \land y \in B) \land x +_{R} y = \underset{˙}{1}) \to y +_{R} x = \underset{˙}{1}$
44	1 16 4	grpsubadd	$⊢ (R \in Grp \land (\underset{˙}{1} \in B \land x \in B \land y \in B)) \to (\underset{˙}{1} \underset{˙}{-} x = y \leftrightarrow y +_{R} x = \underset{˙}{1})$
45	44	biimpar	$⊢ ((R \in Grp \land (\underset{˙}{1} \in B \land x \in B \land y \in B)) \land y +_{R} x = \underset{˙}{1}) \to \underset{˙}{1} \underset{˙}{-} x = y$
46	33 38 43 45	syl21anc	$⊢ ((((R \in NzRing \land x \in B) \land (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U)) \land y \in B) \land x +_{R} y = \underset{˙}{1}) \to \underset{˙}{1} \underset{˙}{-} x = y$
47	46	eqcomd	$⊢ ((((R \in NzRing \land x \in B) \land (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U)) \land y \in B) \land x +_{R} y = \underset{˙}{1}) \to y = \underset{˙}{1} \underset{˙}{-} x$
48	47	adantr	$⊢ (((((R \in NzRing \land x \in B) \land (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U)) \land y \in B) \land x +_{R} y = \underset{˙}{1}) \land \underset{˙}{1} \underset{˙}{-} x \in U) \to y = \underset{˙}{1} \underset{˙}{-} x$
49		simpr	$⊢ (((((R \in NzRing \land x \in B) \land (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U)) \land y \in B) \land x +_{R} y = \underset{˙}{1}) \land \underset{˙}{1} \underset{˙}{-} x \in U) \to \underset{˙}{1} \underset{˙}{-} x \in U$
50	48 49	eqeltrd	$⊢ (((((R \in NzRing \land x \in B) \land (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U)) \land y \in B) \land x +_{R} y = \underset{˙}{1}) \land \underset{˙}{1} \underset{˙}{-} x \in U) \to y \in U$
51		simpllr	$⊢ ((((R \in NzRing \land x \in B) \land (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U)) \land y \in B) \land x +_{R} y = \underset{˙}{1}) \to (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U)$
52	30 50 51	orim12da	$⊢ ((((R \in NzRing \land x \in B) \land (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U)) \land y \in B) \land x +_{R} y = \underset{˙}{1}) \to (x \in U \lor y \in U)$
53	52	ex	$⊢ (((R \in NzRing \land x \in B) \land (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U)) \land y \in B) \to (x +_{R} y = \underset{˙}{1} \to (x \in U \lor y \in U))$
54	53	ralrimiva	$⊢ ((R \in NzRing \land x \in B) \land (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U)) \to \forall y \in B (x +_{R} y = \underset{˙}{1} \to (x \in U \lor y \in U))$
55	54	ex	$⊢ (R \in NzRing \land x \in B) \to ((x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U) \to \forall y \in B (x +_{R} y = \underset{˙}{1} \to (x \in U \lor y \in U)))$
56	55	ralimdva	$⊢ R \in NzRing \to (\forall x \in B (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U) \to \forall x \in B \forall y \in B (x +_{R} y = \underset{˙}{1} \to (x \in U \lor y \in U)))$
57	56	imp	$⊢ (R \in NzRing \land \forall x \in B (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U)) \to \forall x \in B \forall y \in B (x +_{R} y = \underset{˙}{1} \to (x \in U \lor y \in U))$
58	1 16 3 2	islring	$⊢ R \in LRing \leftrightarrow (R \in NzRing \land \forall x \in B \forall y \in B (x +_{R} y = \underset{˙}{1} \to (x \in U \lor y \in U)))$
59	29 57 58	sylanbrc	$⊢ (R \in NzRing \land \forall x \in B (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U)) \to R \in LRing$
60	28 59	impbii	$⊢ R \in LRing \leftrightarrow (R \in NzRing \land \forall x \in B (x \in U \lor \underset{˙}{1} \underset{˙}{-} x \in U))$

Metamath Proof Explorer

Theorem dflring2

Proof