Definition df-lring 13263

Description: A local ring is a nonzero ring where for any two elements summing to one, at least one is invertible. Any field is a local ring; the ring of integers is an example of a ring which is not a local ring. (Contributed by Jim Kingdon, 18-Feb-2025.) (Revised by SN, 23-Feb-2025.)

Assertion

Ref	Expression
df-lring	⊢ LRing = {𝑟 ∈ NzRing ∣ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)((𝑥(+g‘𝑟)𝑦) = (1r‘𝑟) → (𝑥 ∈ (Unit‘𝑟) ∨ 𝑦 ∈ (Unit‘𝑟)))}

Distinct variable group:   𝑥,𝑦,𝑟

Detailed syntax breakdown of Definition df-lring

Step	Hyp	Ref	Expression
1		clring 13262	. 2 class LRing
2		vx	. . . . . . . . 9 setvar 𝑥
3	2	cv 1352	. . . . . . . 8 class 𝑥
4		vy	. . . . . . . . 9 setvar 𝑦
5	4	cv 1352	. . . . . . . 8 class 𝑦
6		vr	. . . . . . . . . 10 setvar 𝑟
7	6	cv 1352	. . . . . . . . 9 class 𝑟
8		cplusg 12528	. . . . . . . . 9 class +g
9	7, 8	cfv 5215	. . . . . . . 8 class (+g‘𝑟)
10	3, 5, 9	co 5872	. . . . . . 7 class (𝑥(+g‘𝑟)𝑦)
11		cur 13073	. . . . . . . 8 class 1r
12	7, 11	cfv 5215	. . . . . . 7 class (1r‘𝑟)
13	10, 12	wceq 1353	. . . . . 6 wff (𝑥(+g‘𝑟)𝑦) = (1r‘𝑟)
14		cui 13187	. . . . . . . . 9 class Unit
15	7, 14	cfv 5215	. . . . . . . 8 class (Unit‘𝑟)
16	3, 15	wcel 2148	. . . . . . 7 wff 𝑥 ∈ (Unit‘𝑟)
17	5, 15	wcel 2148	. . . . . . 7 wff 𝑦 ∈ (Unit‘𝑟)
18	16, 17	wo 708	. . . . . 6 wff (𝑥 ∈ (Unit‘𝑟) ∨ 𝑦 ∈ (Unit‘𝑟))
19	13, 18	wi 4	. . . . 5 wff ((𝑥(+g‘𝑟)𝑦) = (1r‘𝑟) → (𝑥 ∈ (Unit‘𝑟) ∨ 𝑦 ∈ (Unit‘𝑟)))
20		cbs 12454	. . . . . 6 class Base
21	7, 20	cfv 5215	. . . . 5 class (Base‘𝑟)
22	19, 4, 21	wral 2455	. . . 4 wff ∀𝑦 ∈ (Base‘𝑟)((𝑥(+g‘𝑟)𝑦) = (1r‘𝑟) → (𝑥 ∈ (Unit‘𝑟) ∨ 𝑦 ∈ (Unit‘𝑟)))
23	22, 2, 21	wral 2455	. . 3 wff ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)((𝑥(+g‘𝑟)𝑦) = (1r‘𝑟) → (𝑥 ∈ (Unit‘𝑟) ∨ 𝑦 ∈ (Unit‘𝑟)))
24		cnzr 13254	. . 3 class NzRing
25	23, 6, 24	crab 2459	. 2 class {𝑟 ∈ NzRing ∣ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)((𝑥(+g‘𝑟)𝑦) = (1r‘𝑟) → (𝑥 ∈ (Unit‘𝑟) ∨ 𝑦 ∈ (Unit‘𝑟)))}
26	1, 25	wceq 1353	1 wff LRing = {𝑟 ∈ NzRing ∣ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)((𝑥(+g‘𝑟)𝑦) = (1r‘𝑟) → (𝑥 ∈ (Unit‘𝑟) ∨ 𝑦 ∈ (Unit‘𝑟)))}

This definition is referenced by:  islring  13264  lringnzr  13265