Description: The unit 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 ) |