Metamath Proof Explorer


Theorem grplactf1o

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 X a X g + ˙ a
grplact.2 X = Base G
grplact.3 + ˙ = + G
Assertion grplactf1o G Grp A X F A : X 1-1 onto X

Proof

Step Hyp Ref Expression
1 grplact.1 F = g X a X g + ˙ a
2 grplact.2 X = Base G
3 grplact.3 + ˙ = + G
4 eqid inv g G = inv g G
5 1 2 3 4 grplactcnv G Grp A X F A : X 1-1 onto X F A -1 = F inv g G A
6 5 simpld G Grp A X F A : X 1-1 onto X