Theorem gapm

Description: The action of a particular group element is a permutation of the base set. (Contributed by Jeff Hankins, 11-Aug-2009) (Proof shortened by Mario Carneiro, 13-Jan-2015)

	Ref	Expression
Hypotheses	gapm.1	$$⊢X={\mathrm{Base}}_G$$
	gapm.2	$$⊢F=\left(x\in Y⟼A\underset{\dot{}}{\oplus }x\right)$$
Assertion	gapm	$$⊢\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in X\right)\to F:Y\underset{1-1\; onto}{⟶}Y$$

Proof

Step	Hyp	Ref	Expression
1		gapm.1	$$⊢X={\mathrm{Base}}_G$$
2		gapm.2	$$⊢F=\left(x\in Y⟼A\underset{\dot{}}{\oplus }x\right)$$
3	1	gaf	$$⊢\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\to \underset{\dot{}}{\oplus }:X\times Y⟶Y$$
4	3	ad2antrr	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in X\right)\wedge x\in Y\right)\to \underset{\dot{}}{\oplus }:X\times Y⟶Y$$
5		simplr	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in X\right)\wedge x\in Y\right)\to A\in X$$
6		simpr	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in X\right)\wedge x\in Y\right)\to x\in Y$$
7	4 5 6	fovcdmd	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in X\right)\wedge x\in Y\right)\to A\underset{\dot{}}{\oplus }x\in Y$$
8	3	ad2antrr	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in X\right)\wedge y\in Y\right)\to \underset{\dot{}}{\oplus }:X\times Y⟶Y$$
9		gagrp	$$⊢\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\to G\in \mathrm{Grp}$$
10	9	ad2antrr	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in X\right)\wedge y\in Y\right)\to G\in \mathrm{Grp}$$
11		simplr	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in X\right)\wedge y\in Y\right)\to A\in X$$
12		eqid	$$⊢{inv}_g\left(G\right)={inv}_g\left(G\right)$$
13	1 12	grpinvcl	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\right)\to {inv}_g\left(G\right)\left(A\right)\in X$$
14	10 11 13	syl2anc	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in X\right)\wedge y\in Y\right)\to {inv}_g\left(G\right)\left(A\right)\in X$$
15		simpr	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in X\right)\wedge y\in Y\right)\to y\in Y$$
16	8 14 15	fovcdmd	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in X\right)\wedge y\in Y\right)\to {inv}_g\left(G\right)\left(A\right)\underset{\dot{}}{\oplus }y\in Y$$
17		simpll	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in X\right)\wedge \left(x\in Y\wedge y\in Y\right)\right)\to \underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)$$
18		simplr	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in X\right)\wedge \left(x\in Y\wedge y\in Y\right)\right)\to A\in X$$
19		simprl	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in X\right)\wedge \left(x\in Y\wedge y\in Y\right)\right)\to x\in Y$$
20		simprr	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in X\right)\wedge \left(x\in Y\wedge y\in Y\right)\right)\to y\in Y$$
21	1 12	gacan	$$⊢\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge \left(A\in X\wedge x\in Y\wedge y\in Y\right)\right)\to \left(A\underset{\dot{}}{\oplus }x=y\leftrightarrow {inv}_g\left(G\right)\left(A\right)\underset{\dot{}}{\oplus }y=x\right)$$
22	17 18 19 20 21	syl13anc	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in X\right)\wedge \left(x\in Y\wedge y\in Y\right)\right)\to \left(A\underset{\dot{}}{\oplus }x=y\leftrightarrow {inv}_g\left(G\right)\left(A\right)\underset{\dot{}}{\oplus }y=x\right)$$
23	22	bicomd	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in X\right)\wedge \left(x\in Y\wedge y\in Y\right)\right)\to \left({inv}_g\left(G\right)\left(A\right)\underset{\dot{}}{\oplus }y=x\leftrightarrow A\underset{\dot{}}{\oplus }x=y\right)$$
24		eqcom	$$⊢x={inv}_g\left(G\right)\left(A\right)\underset{\dot{}}{\oplus }y\leftrightarrow {inv}_g\left(G\right)\left(A\right)\underset{\dot{}}{\oplus }y=x$$
25		eqcom	$$⊢y=A\underset{\dot{}}{\oplus }x\leftrightarrow A\underset{\dot{}}{\oplus }x=y$$
26	23 24 25	3bitr4g	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in X\right)\wedge \left(x\in Y\wedge y\in Y\right)\right)\to \left(x={inv}_g\left(G\right)\left(A\right)\underset{\dot{}}{\oplus }y\leftrightarrow y=A\underset{\dot{}}{\oplus }x\right)$$
27	2 7 16 26	f1o2d	$$⊢\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in X\right)\to F:Y\underset{1-1\; onto}{⟶}Y$$