Definition df-rlreg 20467

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 20463	. 2 class RLReg
2		vr	. . 3 setvar 𝑟
3		cvv 3422	. . 3 class V
4		vx	. . . . . . . . 9 setvar 𝑥
5	4	cv 1538	. . . . . . . 8 class 𝑥
6		vy	. . . . . . . . 9 setvar 𝑦
7	6	cv 1538	. . . . . . . 8 class 𝑦
8	2	cv 1538	. . . . . . . . 9 class 𝑟
9		cmulr 16889	. . . . . . . . 9 class .r
10	8, 9	cfv 6418	. . . . . . . 8 class (.r‘𝑟)
11	5, 7, 10	co 7255	. . . . . . 7 class (𝑥(.r‘𝑟)𝑦)
12		c0g 17067	. . . . . . . 8 class 0g
13	8, 12	cfv 6418	. . . . . . 7 class (0g‘𝑟)
14	11, 13	wceq 1539	. . . . . 6 wff (𝑥(.r‘𝑟)𝑦) = (0g‘𝑟)
15	7, 13	wceq 1539	. . . . . 6 wff 𝑦 = (0g‘𝑟)
16	14, 15	wi 4	. . . . 5 wff ((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟))
17		cbs 16840	. . . . . 6 class Base
18	8, 17	cfv 6418	. . . . 5 class (Base‘𝑟)
19	16, 6, 18	wral 3063	. . . 4 wff ∀𝑦 ∈ (Base‘𝑟)((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟))
20	19, 4, 18	crab 3067	. . 3 class {𝑥 ∈ (Base‘𝑟) ∣ ∀𝑦 ∈ (Base‘𝑟)((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟))}
21	2, 3, 20	cmpt 5153	. 2 class (𝑟 ∈ V ↦ {𝑥 ∈ (Base‘𝑟) ∣ ∀𝑦 ∈ (Base‘𝑟)((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟))})
22	1, 21	wceq 1539	1 wff RLReg = (𝑟 ∈ V ↦ {𝑥 ∈ (Base‘𝑟) ∣ ∀𝑦 ∈ (Base‘𝑟)((𝑥(.r‘𝑟)𝑦) = (0g‘𝑟) → 𝑦 = (0g‘𝑟))})

This definition is referenced by:  rrgval  20471