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

Definition df-rlreg 18442
 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
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-rlreg
StepHypRef Expression
1 crlreg 18438 . 2 RLReg
2 vr . . 3
3 cvv 3087 . . 3
4 vx . . . . . . . . 9
54cv 1436 . . . . . . . 8
6 vy . . . . . . . . 9
76cv 1436 . . . . . . . 8
82cv 1436 . . . . . . . . 9
9 cmulr 15153 . . . . . . . . 9
108, 9cfv 5601 . . . . . . . 8
115, 7, 10co 6305 . . . . . . 7
12 c0g 15297 . . . . . . . 8
138, 12cfv 5601 . . . . . . 7
1411, 13wceq 1437 . . . . . 6
157, 13wceq 1437 . . . . . 6
1614, 15wi 4 . . . . 5
17 cbs 15084 . . . . . 6
188, 17cfv 5601 . . . . 5
1916, 6, 18wral 2782 . . . 4
2019, 4, 18crab 2786 . . 3
212, 3, 20cmpt 4484 . 2
221, 21wceq 1437 1 RLReg
 Colors of variables: wff setvar class This definition is referenced by:  rrgval  18446
 Copyright terms: Public domain W3C validator