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	Could not format assertion : No typesetting found for |- 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 ) ) ) } with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clring	Could not format LRing : No typesetting found for class LRing with typecode class
1		vr	$$setvarr$$
2		cnzr	$$class\mathrm{NzRing}$$
3		vx	$$setvarx$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarr$$
6	5 4	cfv	$$class{\mathrm{Base}}_r$$
7		vy	$$setvary$$
8	3	cv	$$setvarx$$
9		cplusg	$$class{+}_{𝑔}$$
10	5 9	cfv	$$class{+}_r$$
11	7	cv	$$setvary$$
12	8 11 10	co	$$class\left(x{+}_{r}y\right)$$
13		cur	$$class{1}_r$$
14	5 13	cfv	$$class{1}_r$$
15	12 14	wceq	$$wffx{+}_{r}y=1_r$$
16		cui	$$class\mathrm{Unit}$$
17	5 16	cfv	$$class\mathrm{Unit}\left(r\right)$$
18	8 17	wcel	$$wffx\in \mathrm{Unit}\left(r\right)$$
19	11 17	wcel	$$wffy\in \mathrm{Unit}\left(r\right)$$
20	18 19	wo	$$wff\left(x\in \mathrm{Unit}\left(r\right)\vee y\in \mathrm{Unit}\left(r\right)\right)$$
21	15 20	wi	$$wff\left(x{+}_{r}y=1_r\to \left(x\in \mathrm{Unit}\left(r\right)\vee y\in \mathrm{Unit}\left(r\right)\right)\right)$$
22	21 7 6	wral	$$wff\forall y\in {\mathrm{Base}}_r\left(x{+}_{r}y=1_r\to \left(x\in \mathrm{Unit}\left(r\right)\vee y\in \mathrm{Unit}\left(r\right)\right)\right)$$
23	22 3 6	wral	$$wff\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_r\left(x{+}_{r}y=1_r\to \left(x\in \mathrm{Unit}\left(r\right)\vee y\in \mathrm{Unit}\left(r\right)\right)\right)$$
24	23 1 2	crab	$$class\left\{r\in \mathrm{NzRing}|\forall x\in {\mathrm{Base}}_r\forall y\in {\mathrm{Base}}_r\left(x{+}_{r}y=1_r\to \left(x\in \mathrm{Unit}\left(r\right)\vee y\in \mathrm{Unit}\left(r\right)\right)\right)\right\}$$
25	0 24	wceq	Could not format 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 ) ) ) } : No typesetting found for 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 ) ) ) } with typecode wff