ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-lring Unicode version

Definition df-lring 13263
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
StepHypRef Expression
1 clring 13262 . 2  class LRing
2 vx . . . . . . . . 9  setvar  x
32cv 1352 . . . . . . . 8  class  x
4 vy . . . . . . . . 9  setvar  y
54cv 1352 . . . . . . . 8  class  y
6 vr . . . . . . . . . 10  setvar  r
76cv 1352 . . . . . . . . 9  class  r
8 cplusg 12528 . . . . . . . . 9  class  +g
97, 8cfv 5215 . . . . . . . 8  class  ( +g  `  r )
103, 5, 9co 5872 . . . . . . 7  class  ( x ( +g  `  r
) y )
11 cur 13073 . . . . . . . 8  class  1r
127, 11cfv 5215 . . . . . . 7  class  ( 1r
`  r )
1310, 12wceq 1353 . . . . . 6  wff  ( x ( +g  `  r
) y )  =  ( 1r `  r
)
14 cui 13187 . . . . . . . . 9  class Unit
157, 14cfv 5215 . . . . . . . 8  class  (Unit `  r )
163, 15wcel 2148 . . . . . . 7  wff  x  e.  (Unit `  r )
175, 15wcel 2148 . . . . . . 7  wff  y  e.  (Unit `  r )
1816, 17wo 708 . . . . . 6  wff  ( x  e.  (Unit `  r
)  \/  y  e.  (Unit `  r )
)
1913, 18wi 4 . . . . 5  wff  ( ( x ( +g  `  r
) y )  =  ( 1r `  r
)  ->  ( x  e.  (Unit `  r )  \/  y  e.  (Unit `  r ) ) )
20 cbs 12454 . . . . . 6  class  Base
217, 20cfv 5215 . . . . 5  class  ( Base `  r )
2219, 4, 21wral 2455 . . . 4  wff  A. y  e.  ( Base `  r
) ( ( x ( +g  `  r
) y )  =  ( 1r `  r
)  ->  ( x  e.  (Unit `  r )  \/  y  e.  (Unit `  r ) ) )
2322, 2, 21wral 2455 . . 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 13254 . . 3  class NzRing
2523, 6, 24crab 2459 . 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 ) ) ) }
261, 25wceq 1353 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 ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  islring  13264  lringnzr  13265
  Copyright terms: Public domain W3C validator