This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in X ⟼ (a \in X ⟼ g \underset{˙}{+} a))$
	grplact.2	$⊢ X = {Base}_{G}$
	grplact.3	$⊢ \underset{˙}{+} = +_{G}$
Assertion	grplactf1o	$⊢ (G \in Grp \land A \in X) \to F (A) : X \underset{1-1 onto}{⟶} X$

Proof

Step	Hyp	Ref	Expression
1		grplact.1	$⊢ F = (g \in X ⟼ (a \in X ⟼ g \underset{˙}{+} a))$
2		grplact.2	$⊢ X = {Base}_{G}$
3		grplact.3	$⊢ \underset{˙}{+} = +_{G}$
4		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
5	1 2 3 4	grplactcnv	$⊢ (G \in Grp \land A \in X) \to (F (A) : X \underset{1-1 onto}{⟶} X \land {F (A)}^{-1} = F ({inv}_{g} (G) (A)))$
6	5	simpld	$⊢ (G \in Grp \land A \in X) \to F (A) : X \underset{1-1 onto}{⟶} X$