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 = (𝑟 ∈ V ↦ {𝑥 ∈ (Base‘𝑟) ∣ ∀𝑦 ∈ (Base‘𝑟)((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟))})

Distinct variable group:   𝑥,𝑟,𝑦

Detailed syntax breakdown of Definition df-rlreg

Step	Hyp	Ref	Expression
1		crlreg 13821	. 2 class RLReg
2		vr	. . 3 setvar 𝑟
3		cvv 2763	. . 3 class V
4		vx	. . . . . . . . 9 setvar 𝑥
5	4	cv 1363	. . . . . . . 8 class 𝑥
6		vy	. . . . . . . . 9 setvar 𝑦
7	6	cv 1363	. . . . . . . 8 class 𝑦
8	2	cv 1363	. . . . . . . . 9 class 𝑟
9		cmulr 12766	. . . . . . . . 9 class .r
10	8, 9	cfv 5259	. . . . . . . 8 class (.r‘𝑟)
11	5, 7, 10	co 5923	. . . . . . 7 class (𝑥(.r‘𝑟)𝑦)
12		c0g 12937	. . . . . . . 8 class 0g
13	8, 12	cfv 5259	. . . . . . 7 class (0g‘𝑟)
14	11, 13	wceq 1364	. . . . . 6 wff (𝑥(.r‘𝑟)𝑦) = (0g‘𝑟)
15	7, 13	wceq 1364	. . . . . 6 wff 𝑦 = (0g‘𝑟)
16	14, 15	wi 4	. . . . 5 wff ((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟))
17		cbs 12688	. . . . . 6 class Base
18	8, 17	cfv 5259	. . . . 5 class (Base‘𝑟)
19	16, 6, 18	wral 2475	. . . 4 wff ∀𝑦 ∈ (Base‘𝑟)((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟))
20	19, 4, 18	crab 2479	. . 3 class {𝑥 ∈ (Base‘𝑟) ∣ ∀𝑦 ∈ (Base‘𝑟)((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟))}
21	2, 3, 20	cmpt 4095	. 2 class (𝑟 ∈ V ↦ {𝑥 ∈ (Base‘𝑟) ∣ ∀𝑦 ∈ (Base‘𝑟)((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟))})
22	1, 21	wceq 1364	1 wff RLReg = (𝑟 ∈ V ↦ {𝑥 ∈ (Base‘𝑟) ∣ ∀𝑦 ∈ (Base‘𝑟)((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟))})

This definition is referenced by:  rrgmex  13827  rrgval  13828