Definition df-rlreg

Description: Define the set ofleft-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)

	Ref	Expression
Assertion	df-rlreg	|- RLReg = ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crlreg	|- RLReg
1		vr	|- r
2		cvv	|- _V
3		vx	|- x
4		cbs	|- Base
5	1	cv	|- r
6	5 4	cfv	|- ( Base ` r )
7		vy	|- y
8	3	cv	|- x
9		cmulr	|- .r
10	5 9	cfv	|- ( .r ` r )
11	7	cv	|- y
12	8 11 10	co	|- ( x ( .r ` r ) y )
13		c0g	|- 0g
14	5 13	cfv	|- ( 0g ` r )
15	12 14	wceq	|- ( x ( .r ` r ) y ) = ( 0g ` r )
16	11 14	wceq	|- y = ( 0g ` r )
17	15 16	wi	|- ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) )
18	17 7 6	wral	|- A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) )
19	18 3 6	crab	|- { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) }
20	1 2 19	cmpt	|- ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )
21	0 20	wceq	|- RLReg = ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )