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 = { 𝑟 ∈ NzRing ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) = ( 1r ‘ 𝑟 ) → ( 𝑥 ∈ ( Unit ‘ 𝑟 ) ∨ 𝑦 ∈ ( Unit ‘ 𝑟 ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clring	⊢ LRing
1		vr	⊢ 𝑟
2		cnzr	⊢ NzRing
3		vx	⊢ 𝑥
4		cbs	⊢ Base
5	1	cv	⊢ 𝑟
6	5 4	cfv	⊢ ( Base ‘ 𝑟 )
7		vy	⊢ 𝑦
8	3	cv	⊢ 𝑥
9		cplusg	⊢ +g
10	5 9	cfv	⊢ ( +g ‘ 𝑟 )
11	7	cv	⊢ 𝑦
12	8 11 10	co	⊢ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 )
13		cur	⊢ 1r
14	5 13	cfv	⊢ ( 1r ‘ 𝑟 )
15	12 14	wceq	⊢ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) = ( 1r ‘ 𝑟 )
16		cui	⊢ Unit
17	5 16	cfv	⊢ ( Unit ‘ 𝑟 )
18	8 17	wcel	⊢ 𝑥 ∈ ( Unit ‘ 𝑟 )
19	11 17	wcel	⊢ 𝑦 ∈ ( Unit ‘ 𝑟 )
20	18 19	wo	⊢ ( 𝑥 ∈ ( Unit ‘ 𝑟 ) ∨ 𝑦 ∈ ( Unit ‘ 𝑟 ) )
21	15 20	wi	⊢ ( ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) = ( 1r ‘ 𝑟 ) → ( 𝑥 ∈ ( Unit ‘ 𝑟 ) ∨ 𝑦 ∈ ( Unit ‘ 𝑟 ) ) )
22	21 7 6	wral	⊢ ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) = ( 1r ‘ 𝑟 ) → ( 𝑥 ∈ ( Unit ‘ 𝑟 ) ∨ 𝑦 ∈ ( Unit ‘ 𝑟 ) ) )
23	22 3 6	wral	⊢ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) = ( 1r ‘ 𝑟 ) → ( 𝑥 ∈ ( Unit ‘ 𝑟 ) ∨ 𝑦 ∈ ( Unit ‘ 𝑟 ) ) )
24	23 1 2	crab	⊢ { 𝑟 ∈ NzRing ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) = ( 1r ‘ 𝑟 ) → ( 𝑥 ∈ ( Unit ‘ 𝑟 ) ∨ 𝑦 ∈ ( Unit ‘ 𝑟 ) ) ) }
25	0 24	wceq	⊢ LRing = { 𝑟 ∈ NzRing ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) = ( 1r ‘ 𝑟 ) → ( 𝑥 ∈ ( Unit ‘ 𝑟 ) ∨ 𝑦 ∈ ( Unit ‘ 𝑟 ) ) ) }