Description: The identity element of a group is a left identity. (Contributed by NM, 24-Oct-2006) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | grpoidval.1 | |- X = ran G |
|
| grpoidval.2 | |- U = ( GId ` G ) |
||
| Assertion | grpolid | |- ( ( G e. GrpOp /\ A e. X ) -> ( U G A ) = A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | grpoidval.1 | |- X = ran G |
|
| 2 | grpoidval.2 | |- U = ( GId ` G ) |
|
| 3 | 1 2 | grpoidinv2 | |- ( ( G e. GrpOp /\ A e. X ) -> ( ( ( U G A ) = A /\ ( A G U ) = A ) /\ E. y e. X ( ( y G A ) = U /\ ( A G y ) = U ) ) ) |
| 4 | 3 | simplld | |- ( ( G e. GrpOp /\ A e. X ) -> ( U G A ) = A ) |