Metamath Proof Explorer

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 ∈ NzRing | ∀ x ∈ Base r ∀ y ∈ Base r x + r y = 1 r → x ∈ Unit ⁡ r ∨ y ∈ Unit ⁡ r

Detailed syntax breakdown

Step Hyp Ref Expression
0 clring class LRing
1 vr setvar r
2 cnzr class NzRing
3 vx setvar x
4 cbs class Base
5 1 cv setvar r
6 5 4 cfv class Base r
7 vy setvar y
8 3 cv setvar x
9 cplusg class + 𝑔
10 5 9 cfv class + r
11 7 cv setvar y
12 8 11 10 co class x + r y
13 cur class 1 r
14 5 13 cfv class 1 r
15 12 14 wceq wff x + r y = 1 r
16 cui class Unit
17 5 16 cfv class Unit ⁡ r
18 8 17 wcel wff x ∈ Unit ⁡ r
19 11 17 wcel wff y ∈ Unit ⁡ r
20 18 19 wo wff x ∈ Unit ⁡ r ∨ y ∈ Unit ⁡ r
21 15 20 wi wff x + r y = 1 r → x ∈ Unit ⁡ r ∨ y ∈ Unit ⁡ r
22 21 7 6 wral wff ∀ y ∈ Base r x + r y = 1 r → x ∈ Unit ⁡ r ∨ y ∈ Unit ⁡ r
23 22 3 6 wral wff ∀ x ∈ Base r ∀ y ∈ Base r x + r y = 1 r → x ∈ Unit ⁡ r ∨ y ∈ Unit ⁡ r
24 23 1 2 crab class r ∈ NzRing | ∀ x ∈ Base r ∀ y ∈ Base r x + r y = 1 r → x ∈ Unit ⁡ r ∨ y ∈ Unit ⁡ r
25 0 24 wceq wff LRing = r ∈ NzRing | ∀ x ∈ Base r ∀ y ∈ Base r x + r y = 1 r → x ∈ Unit ⁡ r ∨ y ∈ Unit ⁡ r