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=\left(g\in X⟼\left(a\in X⟼g\underset{\dot{}}{+}a\right)\right)$$
	grplact.2	$$⊢X={\mathrm{Base}}_G$$
	grplact.3	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	grplactf1o	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\right)\to F\left(A\right):X\underset{1-1\; onto}{⟶}X$$

Proof

Step	Hyp	Ref	Expression
1		grplact.1	$$⊢F=\left(g\in X⟼\left(a\in X⟼g\underset{\dot{}}{+}a\right)\right)$$
2		grplact.2	$$⊢X={\mathrm{Base}}_G$$
3		grplact.3	$$⊢\underset{\dot{}}{+}={+}_G$$
4		eqid	$$⊢{inv}_g\left(G\right)={inv}_g\left(G\right)$$
5	1 2 3 4	grplactcnv	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\right)\to \left(F\left(A\right):X\underset{1-1\; onto}{⟶}X\wedge {F\left(A\right)}^{-1}=F\left({inv}_g\left(G\right)\left(A\right)\right)\right)$$
6	5	simpld	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\right)\to F\left(A\right):X\underset{1-1\; onto}{⟶}X$$