Description: The left group action of element A of group G maps the underlying set X of G one-to-one onto itself. (Contributed by Paul Chapman, 18-Mar-2008) (Proof shortened by Mario Carneiro, 14-Aug-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | grplact.1 | |- F = ( g e. X |-> ( a e. X |-> ( g .+ a ) ) ) |
|
| grplact.2 | |- X = ( Base ` G ) |
||
| grplact.3 | |- .+ = ( +g ` G ) |
||
| Assertion | grplactf1o | |- ( ( G e. Grp /\ A e. X ) -> ( F ` A ) : X -1-1-onto-> X ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | grplact.1 | |- F = ( g e. X |-> ( a e. X |-> ( g .+ a ) ) ) |
|
| 2 | grplact.2 | |- X = ( Base ` G ) |
|
| 3 | grplact.3 | |- .+ = ( +g ` G ) |
|
| 4 | eqid | |- ( invg ` G ) = ( invg ` G ) |
|
| 5 | 1 2 3 4 | grplactcnv | |- ( ( G e. Grp /\ A e. X ) -> ( ( F ` A ) : X -1-1-onto-> X /\ `' ( F ` A ) = ( F ` ( ( invg ` G ) ` A ) ) ) ) |
| 6 | 5 | simpld | |- ( ( G e. Grp /\ A e. X ) -> ( F ` A ) : X -1-1-onto-> X ) |