Definition df-lring 13747

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 = { r e. NzRing | A. x e. ( Base ` r ) A. y e. ( Base ` r ) ( ( x ( +g ` r ) y ) = ( 1r ` r ) -> ( x e. (Unit ` r ) \/ y e. (Unit ` r ) ) ) }

Distinct variable group:   x, y, r

Detailed syntax breakdown of Definition df-lring

Step	Hyp	Ref	Expression
1		clring 13746	. 2 class LRing
2		vx	. . . . . . . . 9 setvar x
3	2	cv 1363	. . . . . . . 8 class x
4		vy	. . . . . . . . 9 setvar y
5	4	cv 1363	. . . . . . . 8 class y
6		vr	. . . . . . . . . 10 setvar r
7	6	cv 1363	. . . . . . . . 9 class r
8		cplusg 12755	. . . . . . . . 9 class +g
9	7, 8	cfv 5258	. . . . . . . 8 class ( +g ` r )
10	3, 5, 9	co 5922	. . . . . . 7 class ( x ( +g ` r ) y )
11		cur 13515	. . . . . . . 8 class 1r
12	7, 11	cfv 5258	. . . . . . 7 class ( 1r ` r )
13	10, 12	wceq 1364	. . . . . 6 wff ( x ( +g ` r ) y ) = ( 1r ` r )
14		cui 13643	. . . . . . . . 9 class Unit
15	7, 14	cfv 5258	. . . . . . . 8 class (Unit ` r )
16	3, 15	wcel 2167	. . . . . . 7 wff x e. (Unit ` r )
17	5, 15	wcel 2167	. . . . . . 7 wff y e. (Unit ` r )
18	16, 17	wo 709	. . . . . 6 wff ( x e. (Unit ` r ) \/ y e. (Unit ` r ) )
19	13, 18	wi 4	. . . . 5 wff ( ( x ( +g ` r ) y ) = ( 1r ` r ) -> ( x e. (Unit ` r ) \/ y e. (Unit ` r ) ) )
20		cbs 12678	. . . . . 6 class Base
21	7, 20	cfv 5258	. . . . 5 class ( Base ` r )
22	19, 4, 21	wral 2475	. . . 4 wff A. y e. ( Base ` r ) ( ( x ( +g ` r ) y ) = ( 1r ` r ) -> ( x e. (Unit ` r ) \/ y e. (Unit ` r ) ) )
23	22, 2, 21	wral 2475	. . 3 wff A. x e. ( Base ` r ) A. y e. ( Base ` r ) ( ( x ( +g ` r ) y ) = ( 1r ` r ) -> ( x e. (Unit ` r ) \/ y e. (Unit ` r ) ) )
24		cnzr 13735	. . 3 class NzRing
25	23, 6, 24	crab 2479	. 2 class { r e. NzRing | A. x e. ( Base ` r ) A. y e. ( Base ` r ) ( ( x ( +g ` r ) y ) = ( 1r ` r ) -> ( x e. (Unit ` r ) \/ y e. (Unit ` r ) ) ) }
26	1, 25	wceq 1364	1 wff LRing = { r e. NzRing | A. x e. ( Base ` r ) A. y e. ( Base ` r ) ( ( x ( +g ` r ) y ) = ( 1r ` r ) -> ( x e. (Unit ` r ) \/ y e. (Unit ` r ) ) ) }

This definition is referenced by:  islring  13748  lringnzr  13749