Definition df-lring

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)

	Ref	Expression
Assertion	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 ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clring	|- LRing
1		vr	|- r
2		cnzr	|- NzRing
3		vx	|- x
4		cbs	|- Base
5	1	cv	|- r
6	5 4	cfv	|- ( Base ` r )
7		vy	|- y
8	3	cv	|- x
9		cplusg	|- +g
10	5 9	cfv	|- ( +g ` r )
11	7	cv	|- y
12	8 11 10	co	|- ( x ( +g ` r ) y )
13		cur	|- 1r
14	5 13	cfv	|- ( 1r ` r )
15	12 14	wceq	|- ( x ( +g ` r ) y ) = ( 1r ` r )
16		cui	|- Unit
17	5 16	cfv	|- ( Unit ` r )
18	8 17	wcel	|- x e. ( Unit ` r )
19	11 17	wcel	|- y e. ( Unit ` r )
20	18 19	wo	|- ( x e. ( Unit ` r ) \/ y e. ( Unit ` r ) )
21	15 20	wi	|- ( ( x ( +g ` r ) y ) = ( 1r ` r ) -> ( x e. ( Unit ` r ) \/ y e. ( Unit ` r ) ) )
22	21 7 6	wral	|- A. y e. ( Base ` r ) ( ( x ( +g ` r ) y ) = ( 1r ` r ) -> ( x e. ( Unit ` r ) \/ y e. ( Unit ` r ) ) )
23	22 3 6	wral	|- 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	23 1 2	crab	|- { 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 ) ) ) }
25	0 24	wceq	|- 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 ) ) ) }