Definition df-rlreg 13824

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 = ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )

Distinct variable group:   x, r, y

Detailed syntax breakdown of Definition df-rlreg

Step	Hyp	Ref	Expression
1		crlreg 13821	. 2 class RLReg
2		vr	. . 3 setvar r
3		cvv 2763	. . 3 class _V
4		vx	. . . . . . . . 9 setvar x
5	4	cv 1363	. . . . . . . 8 class x
6		vy	. . . . . . . . 9 setvar y
7	6	cv 1363	. . . . . . . 8 class y
8	2	cv 1363	. . . . . . . . 9 class r
9		cmulr 12766	. . . . . . . . 9 class .r
10	8, 9	cfv 5259	. . . . . . . 8 class ( .r ` r )
11	5, 7, 10	co 5923	. . . . . . 7 class ( x ( .r ` r ) y )
12		c0g 12937	. . . . . . . 8 class 0g
13	8, 12	cfv 5259	. . . . . . 7 class ( 0g ` r )
14	11, 13	wceq 1364	. . . . . 6 wff ( x ( .r ` r ) y ) = ( 0g ` r )
15	7, 13	wceq 1364	. . . . . 6 wff y = ( 0g ` r )
16	14, 15	wi 4	. . . . 5 wff ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) )
17		cbs 12688	. . . . . 6 class Base
18	8, 17	cfv 5259	. . . . 5 class ( Base ` r )
19	16, 6, 18	wral 2475	. . . 4 wff A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) )
20	19, 4, 18	crab 2479	. . 3 class { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) }
21	2, 3, 20	cmpt 4095	. 2 class ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )
22	1, 21	wceq 1364	1 wff RLReg = ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )

This definition is referenced by:  rrgmex  13827  rrgval  13828