This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑟 ) ) } )