ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-lring GIF 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 = {π‘Ÿ ∈ NzRing ∣ βˆ€π‘₯ ∈ (Baseβ€˜π‘Ÿ)βˆ€π‘¦ ∈ (Baseβ€˜π‘Ÿ)((π‘₯(+gβ€˜π‘Ÿ)𝑦) = (1rβ€˜π‘Ÿ) β†’ (π‘₯ ∈ (Unitβ€˜π‘Ÿ) ∨ 𝑦 ∈ (Unitβ€˜π‘Ÿ)))}
Distinct variable group:   π‘₯,𝑦,π‘Ÿ

Detailed syntax breakdown of Definition df-lring
StepHypRef Expression
1 clring 13262 . 2 class LRing
2 vx . . . . . . . . 9 setvar π‘₯
32cv 1352 . . . . . . . 8 class π‘₯
4 vy . . . . . . . . 9 setvar 𝑦
54cv 1352 . . . . . . . 8 class 𝑦
6 vr . . . . . . . . . 10 setvar π‘Ÿ
76cv 1352 . . . . . . . . 9 class π‘Ÿ
8 cplusg 12528 . . . . . . . . 9 class +g
97, 8cfv 5215 . . . . . . . 8 class (+gβ€˜π‘Ÿ)
103, 5, 9co 5872 . . . . . . 7 class (π‘₯(+gβ€˜π‘Ÿ)𝑦)
11 cur 13073 . . . . . . . 8 class 1r
127, 11cfv 5215 . . . . . . 7 class (1rβ€˜π‘Ÿ)
1310, 12wceq 1353 . . . . . 6 wff (π‘₯(+gβ€˜π‘Ÿ)𝑦) = (1rβ€˜π‘Ÿ)
14 cui 13187 . . . . . . . . 9 class Unit
157, 14cfv 5215 . . . . . . . 8 class (Unitβ€˜π‘Ÿ)
163, 15wcel 2148 . . . . . . 7 wff π‘₯ ∈ (Unitβ€˜π‘Ÿ)
175, 15wcel 2148 . . . . . . 7 wff 𝑦 ∈ (Unitβ€˜π‘Ÿ)
1816, 17wo 708 . . . . . 6 wff (π‘₯ ∈ (Unitβ€˜π‘Ÿ) ∨ 𝑦 ∈ (Unitβ€˜π‘Ÿ))
1913, 18wi 4 . . . . 5 wff ((π‘₯(+gβ€˜π‘Ÿ)𝑦) = (1rβ€˜π‘Ÿ) β†’ (π‘₯ ∈ (Unitβ€˜π‘Ÿ) ∨ 𝑦 ∈ (Unitβ€˜π‘Ÿ)))
20 cbs 12454 . . . . . 6 class Base
217, 20cfv 5215 . . . . 5 class (Baseβ€˜π‘Ÿ)
2219, 4, 21wral 2455 . . . 4 wff βˆ€π‘¦ ∈ (Baseβ€˜π‘Ÿ)((π‘₯(+gβ€˜π‘Ÿ)𝑦) = (1rβ€˜π‘Ÿ) β†’ (π‘₯ ∈ (Unitβ€˜π‘Ÿ) ∨ 𝑦 ∈ (Unitβ€˜π‘Ÿ)))
2322, 2, 21wral 2455 . . 3 wff βˆ€π‘₯ ∈ (Baseβ€˜π‘Ÿ)βˆ€π‘¦ ∈ (Baseβ€˜π‘Ÿ)((π‘₯(+gβ€˜π‘Ÿ)𝑦) = (1rβ€˜π‘Ÿ) β†’ (π‘₯ ∈ (Unitβ€˜π‘Ÿ) ∨ 𝑦 ∈ (Unitβ€˜π‘Ÿ)))
24 cnzr 13254 . . 3 class NzRing
2523, 6, 24crab 2459 . 2 class {π‘Ÿ ∈ NzRing ∣ βˆ€π‘₯ ∈ (Baseβ€˜π‘Ÿ)βˆ€π‘¦ ∈ (Baseβ€˜π‘Ÿ)((π‘₯(+gβ€˜π‘Ÿ)𝑦) = (1rβ€˜π‘Ÿ) β†’ (π‘₯ ∈ (Unitβ€˜π‘Ÿ) ∨ 𝑦 ∈ (Unitβ€˜π‘Ÿ)))}
261, 25wceq 1353 1 wff LRing = {π‘Ÿ ∈ NzRing ∣ βˆ€π‘₯ ∈ (Baseβ€˜π‘Ÿ)βˆ€π‘¦ ∈ (Baseβ€˜π‘Ÿ)((π‘₯(+gβ€˜π‘Ÿ)𝑦) = (1rβ€˜π‘Ÿ) β†’ (π‘₯ ∈ (Unitβ€˜π‘Ÿ) ∨ 𝑦 ∈ (Unitβ€˜π‘Ÿ)))}
Colors of variables: wff set class
This definition is referenced by:  islring  13264  lringnzr  13265
  Copyright terms: Public domain W3C validator