MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rlreg Structured version   Visualization version   GIF version

Definition df-rlreg 19050
Description: Define the set of left-regular elements in a ring as those elements which are not left zero divisors, meaning that multiplying a nonzero element on the left by a left-regular element gives a nonzero product. (Contributed by Stefan O'Rear, 22-Mar-2015.)
Assertion
Ref Expression
df-rlreg RLReg = (𝑟 ∈ V ↦ {𝑥 ∈ (Base‘𝑟) ∣ ∀𝑦 ∈ (Base‘𝑟)((𝑥(.r𝑟)𝑦) = (0g𝑟) → 𝑦 = (0g𝑟))})
Distinct variable group:   𝑥,𝑟,𝑦

Detailed syntax breakdown of Definition df-rlreg
StepHypRef Expression
1 crlreg 19046 . 2 class RLReg
2 vr . . 3 setvar 𝑟
3 cvv 3172 . . 3 class V
4 vx . . . . . . . . 9 setvar 𝑥
54cv 1473 . . . . . . . 8 class 𝑥
6 vy . . . . . . . . 9 setvar 𝑦
76cv 1473 . . . . . . . 8 class 𝑦
82cv 1473 . . . . . . . . 9 class 𝑟
9 cmulr 15715 . . . . . . . . 9 class .r
108, 9cfv 5790 . . . . . . . 8 class (.r𝑟)
115, 7, 10co 6527 . . . . . . 7 class (𝑥(.r𝑟)𝑦)
12 c0g 15869 . . . . . . . 8 class 0g
138, 12cfv 5790 . . . . . . 7 class (0g𝑟)
1411, 13wceq 1474 . . . . . 6 wff (𝑥(.r𝑟)𝑦) = (0g𝑟)
157, 13wceq 1474 . . . . . 6 wff 𝑦 = (0g𝑟)
1614, 15wi 4 . . . . 5 wff ((𝑥(.r𝑟)𝑦) = (0g𝑟) → 𝑦 = (0g𝑟))
17 cbs 15641 . . . . . 6 class Base
188, 17cfv 5790 . . . . 5 class (Base‘𝑟)
1916, 6, 18wral 2895 . . . 4 wff 𝑦 ∈ (Base‘𝑟)((𝑥(.r𝑟)𝑦) = (0g𝑟) → 𝑦 = (0g𝑟))
2019, 4, 18crab 2899 . . 3 class {𝑥 ∈ (Base‘𝑟) ∣ ∀𝑦 ∈ (Base‘𝑟)((𝑥(.r𝑟)𝑦) = (0g𝑟) → 𝑦 = (0g𝑟))}
212, 3, 20cmpt 4637 . 2 class (𝑟 ∈ V ↦ {𝑥 ∈ (Base‘𝑟) ∣ ∀𝑦 ∈ (Base‘𝑟)((𝑥(.r𝑟)𝑦) = (0g𝑟) → 𝑦 = (0g𝑟))})
221, 21wceq 1474 1 wff RLReg = (𝑟 ∈ V ↦ {𝑥 ∈ (Base‘𝑟) ∣ ∀𝑦 ∈ (Base‘𝑟)((𝑥(.r𝑟)𝑦) = (0g𝑟) → 𝑦 = (0g𝑟))})
Colors of variables: wff setvar class
This definition is referenced by:  rrgval  19054
  Copyright terms: Public domain W3C validator