Description: The multiplicative identity is the unique element of the ring that is left- and right-neutral on all elements under multiplication. (Contributed by Mario Carneiro, 10-Jan-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | dfur2.b | |- B = ( Base ` R ) |
|
| dfur2.t | |- .x. = ( .r ` R ) |
||
| dfur2.u | |- .1. = ( 1r ` R ) |
||
| Assertion | dfur2 | |- .1. = ( iota e ( e e. B /\ A. x e. B ( ( e .x. x ) = x /\ ( x .x. e ) = x ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfur2.b | |- B = ( Base ` R ) |
|
| 2 | dfur2.t | |- .x. = ( .r ` R ) |
|
| 3 | dfur2.u | |- .1. = ( 1r ` R ) |
|
| 4 | eqid | |- ( mulGrp ` R ) = ( mulGrp ` R ) |
|
| 5 | 4 1 | mgpbas | |- B = ( Base ` ( mulGrp ` R ) ) |
| 6 | 4 2 | mgpplusg | |- .x. = ( +g ` ( mulGrp ` R ) ) |
| 7 | 4 3 | ringidval | |- .1. = ( 0g ` ( mulGrp ` R ) ) |
| 8 | 5 6 7 | grpidval | |- .1. = ( iota e ( e e. B /\ A. x e. B ( ( e .x. x ) = x /\ ( x .x. e ) = x ) ) ) |