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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crlreg	⊢ RLReg
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		cbs	⊢ Base
5	1	cv	⊢ 𝑟
6	5 4	cfv	⊢ ( Base ‘ 𝑟 )
7		vy	⊢ 𝑦
8	3	cv	⊢ 𝑥
9		cmulr	⊢ .r
10	5 9	cfv	⊢ ( .r ‘ 𝑟 )
11	7	cv	⊢ 𝑦
12	8 11 10	co	⊢ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 )
13		c0g	⊢ 0g
14	5 13	cfv	⊢ ( 0g ‘ 𝑟 )
15	12 14	wceq	⊢ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = ( 0g ‘ 𝑟 )
16	11 14	wceq	⊢ 𝑦 = ( 0g ‘ 𝑟 )
17	15 16	wi	⊢ ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = ( 0g ‘ 𝑟 ) → 𝑦 = ( 0g ‘ 𝑟 ) )
18	17 7 6	wral	⊢ ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = ( 0g ‘ 𝑟 ) → 𝑦 = ( 0g ‘ 𝑟 ) )
19	18 3 6	crab	⊢ { 𝑥 ∈ ( Base ‘ 𝑟 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = ( 0g ‘ 𝑟 ) → 𝑦 = ( 0g ‘ 𝑟 ) ) }
20	1 2 19	cmpt	⊢ ( 𝑟 ∈ V ↦ { 𝑥 ∈ ( Base ‘ 𝑟 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = ( 0g ‘ 𝑟 ) → 𝑦 = ( 0g ‘ 𝑟 ) ) } )
21	0 20	wceq	⊢ RLReg = ( 𝑟 ∈ V ↦ { 𝑥 ∈ ( Base ‘ 𝑟 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = ( 0g ‘ 𝑟 ) → 𝑦 = ( 0g ‘ 𝑟 ) ) } )