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	$$⊢\mathrm{RLReg}=\left(r\in \mathrm{V}⟼\left\{x\in {\mathrm{Base}}_r|\forall y\in {\mathrm{Base}}_r\left(x{\cdot }_{r}y=0_r\to y=0_r\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crlreg	$$class\mathrm{RLReg}$$
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarr$$
6	5 4	cfv	$$class{\mathrm{Base}}_r$$
7		vy	$$setvary$$
8	3	cv	$$setvarx$$
9		cmulr	$$class{\cdot }_{𝑟}$$
10	5 9	cfv	$$class{\cdot }_r$$
11	7	cv	$$setvary$$
12	8 11 10	co	$$class\left(x{\cdot }_{r}y\right)$$
13		c0g	$$class{0}_{𝑔}$$
14	5 13	cfv	$$class{0}_r$$
15	12 14	wceq	$$wffx{\cdot }_{r}y=0_r$$
16	11 14	wceq	$$wffy=0_r$$
17	15 16	wi	$$wff\left(x{\cdot }_{r}y=0_r\to y=0_r\right)$$
18	17 7 6	wral	$$wff\forall y\in {\mathrm{Base}}_r\left(x{\cdot }_{r}y=0_r\to y=0_r\right)$$
19	18 3 6	crab	$$class\left\{x\in {\mathrm{Base}}_r|\forall y\in {\mathrm{Base}}_r\left(x{\cdot }_{r}y=0_r\to y=0_r\right)\right\}$$
20	1 2 19	cmpt	$$class\left(r\in \mathrm{V}⟼\left\{x\in {\mathrm{Base}}_r|\forall y\in {\mathrm{Base}}_r\left(x{\cdot }_{r}y=0_r\to y=0_r\right)\right\}\right)$$
21	0 20	wceq	$$wff\mathrm{RLReg}=\left(r\in \mathrm{V}⟼\left\{x\in {\mathrm{Base}}_r|\forall y\in {\mathrm{Base}}_r\left(x{\cdot }_{r}y=0_r\to y=0_r\right)\right\}\right)$$