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 = ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 crlreg 
 |-  RLReg
1 vr 
 |-  r
2 cvv 
 |-  _V
3 vx 
 |-  x
4 cbs 
 |-  Base
5 1 cv 
 |-  r
6 5 4 cfv 
 |-  ( Base ` r )
7 vy 
 |-  y
8 3 cv 
 |-  x
9 cmulr 
 |-  .r
10 5 9 cfv 
 |-  ( .r ` r )
11 7 cv 
 |-  y
12 8 11 10 co 
 |-  ( x ( .r ` r ) y )
13 c0g 
 |-  0g
14 5 13 cfv 
 |-  ( 0g ` r )
15 12 14 wceq 
 |-  ( x ( .r ` r ) y ) = ( 0g ` r )
16 11 14 wceq 
 |-  y = ( 0g ` r )
17 15 16 wi 
 |-  ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) )
18 17 7 6 wral 
 |-  A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) )
19 18 3 6 crab 
 |-  { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) }
20 1 2 19 cmpt 
 |-  ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )
21 0 20 wceq 
 |-  RLReg = ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )