Theorem orbsta2

Description: Relation between the size of the orbit and the size of the stabilizer of a point in a finite group action. (Contributed by Mario Carneiro, 16-Jan-2015)

	Ref	Expression
Hypotheses	orbsta2.x	$$⊢X={\mathrm{Base}}_G$$
	orbsta2.h	$$⊢H=\left\{u\in X|u\underset{\dot{}}{\oplus }A=A\right\}$$
	orbsta2.r	$$⊢\underset{\dot{}}{\sim }=G{~}_{\mathit{QG}}H$$
	orbsta2.o	$$⊢O=\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq Y\wedge \exists g\in Xg\underset{\dot{}}{\oplus }x=y\right)\right\}$$
Assertion	orbsta2	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in Y\right)\wedge X\in \mathrm{Fin}\right)\to \left|X\right|=\left|\left[A\right]O\right|\left|H\right|$$

Proof

Step	Hyp	Ref	Expression
1		orbsta2.x	$$⊢X={\mathrm{Base}}_G$$
2		orbsta2.h	$$⊢H=\left\{u\in X|u\underset{\dot{}}{\oplus }A=A\right\}$$
3		orbsta2.r	$$⊢\underset{\dot{}}{\sim }=G{~}_{\mathit{QG}}H$$
4		orbsta2.o	$$⊢O=\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq Y\wedge \exists g\in Xg\underset{\dot{}}{\oplus }x=y\right)\right\}$$
5	1 2	gastacl	$$⊢\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in Y\right)\to H\in \mathrm{SubGrp}\left(G\right)$$
6	5	adantr	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in Y\right)\wedge X\in \mathrm{Fin}\right)\to H\in \mathrm{SubGrp}\left(G\right)$$
7		simpr	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in Y\right)\wedge X\in \mathrm{Fin}\right)\to X\in \mathrm{Fin}$$
8	1 3 6 7	lagsubg2	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in Y\right)\wedge X\in \mathrm{Fin}\right)\to \left|X\right|=\left|X/\underset{\dot{}}{\sim }\right|\left|H\right|$$
9		pwfi	$$⊢X\in \mathrm{Fin}\leftrightarrow 𝒫X\in \mathrm{Fin}$$
10	7 9	sylib	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in Y\right)\wedge X\in \mathrm{Fin}\right)\to 𝒫X\in \mathrm{Fin}$$
11	1 3	eqger	$$⊢H\in \mathrm{SubGrp}\left(G\right)\to \underset{\dot{}}{\sim }\mathrm{Er}X$$
12	6 11	syl	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in Y\right)\wedge X\in \mathrm{Fin}\right)\to \underset{\dot{}}{\sim }\mathrm{Er}X$$
13	12	qsss	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in Y\right)\wedge X\in \mathrm{Fin}\right)\to X/\underset{\dot{}}{\sim }\subseteq 𝒫X$$
14	10 13	ssfid	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in Y\right)\wedge X\in \mathrm{Fin}\right)\to X/\underset{\dot{}}{\sim }\in \mathrm{Fin}$$
15		eqid	$$⊢\mathrm{ran}\left(k\in X⟼⟨\left[k\right]\underset{\dot{}}{\sim },k\underset{\dot{}}{\oplus }A⟩\right)=\mathrm{ran}\left(k\in X⟼⟨\left[k\right]\underset{\dot{}}{\sim },k\underset{\dot{}}{\oplus }A⟩\right)$$
16	1 2 3 15 4	orbsta	$$⊢\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in Y\right)\to \mathrm{ran}\left(k\in X⟼⟨\left[k\right]\underset{\dot{}}{\sim },k\underset{\dot{}}{\oplus }A⟩\right):X/\underset{\dot{}}{\sim }\underset{1-1\; onto}{⟶}\left[A\right]O$$
17	16	adantr	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in Y\right)\wedge X\in \mathrm{Fin}\right)\to \mathrm{ran}\left(k\in X⟼⟨\left[k\right]\underset{\dot{}}{\sim },k\underset{\dot{}}{\oplus }A⟩\right):X/\underset{\dot{}}{\sim }\underset{1-1\; onto}{⟶}\left[A\right]O$$
18	14 17	hasheqf1od	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in Y\right)\wedge X\in \mathrm{Fin}\right)\to \left|X/\underset{\dot{}}{\sim }\right|=\left|\left[A\right]O\right|$$
19	18	oveq1d	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in Y\right)\wedge X\in \mathrm{Fin}\right)\to \left|X/\underset{\dot{}}{\sim }\right|\left|H\right|=\left|\left[A\right]O\right|\left|H\right|$$
20	8 19	eqtrd	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge A\in Y\right)\wedge X\in \mathrm{Fin}\right)\to \left|X\right|=\left|\left[A\right]O\right|\left|H\right|$$