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 \in V ⟼ \{x \in {Base}_{r} \| \forall y \in {Base}_{r} (x \cdot_{r} y = 0_{r} \to y = 0_{r})\})$

Detailed syntax breakdown

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

Metamath Proof Explorer

Definition df-rlreg

Detailed syntax breakdown