Description: The unity element of a semiring is a right multiplicative identity. (Contributed by NM, 15-Sep-2011) (Revised by Thierry Arnoux, 1-Apr-2018)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | srgidm.b | |- B = ( Base ` R ) |
|
| srgidm.t | |- .x. = ( .r ` R ) |
||
| srgidm.u | |- .1. = ( 1r ` R ) |
||
| Assertion | srgridm | |- ( ( R e. SRing /\ X e. B ) -> ( X .x. .1. ) = X ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | srgidm.b | |- B = ( Base ` R ) |
|
| 2 | srgidm.t | |- .x. = ( .r ` R ) |
|
| 3 | srgidm.u | |- .1. = ( 1r ` R ) |
|
| 4 | 1 2 3 | srgidmlem | |- ( ( R e. SRing /\ X e. B ) -> ( ( .1. .x. X ) = X /\ ( X .x. .1. ) = X ) ) |
| 5 | 4 | simprd | |- ( ( R e. SRing /\ X e. B ) -> ( X .x. .1. ) = X ) |