Description: The unit of a ring is an identity element for the multiplication. (Contributed by FL, 18Apr2010) (New usage is discouraged.)
Ref  Expression  

Hypotheses  uridm.1   H = ( 2nd ` R ) 

uridm.2   X = ran ( 1st ` R ) 

uridm.3   U = ( GId ` H ) 

Assertion  rngolidm   ( ( R e. RingOps /\ A e. X ) > ( U H A ) = A ) 
Step  Hyp  Ref  Expression 

1  uridm.1   H = ( 2nd ` R ) 

2  uridm.2   X = ran ( 1st ` R ) 

3  uridm.3   U = ( GId ` H ) 

4  1 2 3  rngoidmlem   ( ( R e. RingOps /\ A e. X ) > ( ( U H A ) = A /\ ( A H U ) = A ) ) 
5  4  simpld   ( ( R e. RingOps /\ A e. X ) > ( U H A ) = A ) 