Description: The unit of a ring is an identity element for the multiplication. (Contributed by FL, 18-Apr-2010) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | uridm.1 | |- H = ( 2nd ` R ) |
|
uridm.2 | |- X = ran ( 1st ` R ) |
||
uridm2.2 | |- U = ( GId ` H ) |
||
Assertion | rngoridm | |- ( ( R e. RingOps /\ A e. X ) -> ( A H U ) = A ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uridm.1 | |- H = ( 2nd ` R ) |
|
2 | uridm.2 | |- X = ran ( 1st ` R ) |
|
3 | uridm2.2 | |- U = ( GId ` H ) |
|
4 | 1 2 3 | rngoidmlem | |- ( ( R e. RingOps /\ A e. X ) -> ( ( U H A ) = A /\ ( A H U ) = A ) ) |
5 | 4 | simprd | |- ( ( R e. RingOps /\ A e. X ) -> ( A H U ) = A ) |