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	⊢ 𝑋 = ( Base ‘ 𝐺 )
	orbsta2.h	⊢ 𝐻 = { 𝑢 ∈ 𝑋 ∣ ( 𝑢 ⊕ 𝐴 ) = 𝐴 }
	orbsta2.r	⊢ ∼ = ( 𝐺 ~QG 𝐻 )
	orbsta2.o	⊢ 𝑂 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑌 ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) }
Assertion	orbsta2	⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑋 ∈ Fin ) → ( ♯ ‘ 𝑋 ) = ( ( ♯ ‘ [ 𝐴 ] 𝑂 ) · ( ♯ ‘ 𝐻 ) ) )

Proof

Step	Hyp	Ref	Expression
1		orbsta2.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		orbsta2.h	⊢ 𝐻 = { 𝑢 ∈ 𝑋 ∣ ( 𝑢 ⊕ 𝐴 ) = 𝐴 }
3		orbsta2.r	⊢ ∼ = ( 𝐺 ~QG 𝐻 )
4		orbsta2.o	⊢ 𝑂 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑌 ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) }
5	1 2	gastacl	⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )
6	5	adantr	⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑋 ∈ Fin ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )
7		simpr	⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑋 ∈ Fin ) → 𝑋 ∈ Fin )
8	1 3 6 7	lagsubg2	⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑋 ∈ Fin ) → ( ♯ ‘ 𝑋 ) = ( ( ♯ ‘ ( 𝑋 / ∼ ) ) · ( ♯ ‘ 𝐻 ) ) )
9		pwfi	⊢ ( 𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin )
10	9	bilani	⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑋 ∈ Fin ) → 𝒫 𝑋 ∈ Fin )
11	1 3	eqger	⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → ∼ Er 𝑋 )
12	6 11	syl	⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑋 ∈ Fin ) → ∼ Er 𝑋 )
13	12	qsss	⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑋 ∈ Fin ) → ( 𝑋 / ∼ ) ⊆ 𝒫 𝑋 )
14	10 13	ssfid	⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑋 ∈ Fin ) → ( 𝑋 / ∼ ) ∈ Fin )
15		eqid	⊢ ran ( 𝑘 ∈ 𝑋 ↦ ⟨ [ 𝑘 ] ∼ , ( 𝑘 ⊕ 𝐴 ) ⟩ ) = ran ( 𝑘 ∈ 𝑋 ↦ ⟨ [ 𝑘 ] ∼ , ( 𝑘 ⊕ 𝐴 ) ⟩ )
16	1 2 3 15 4	orbsta	⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → ran ( 𝑘 ∈ 𝑋 ↦ ⟨ [ 𝑘 ] ∼ , ( 𝑘 ⊕ 𝐴 ) ⟩ ) : ( 𝑋 / ∼ ) –1-1-onto→ [ 𝐴 ] 𝑂 )
17	16	adantr	⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑋 ∈ Fin ) → ran ( 𝑘 ∈ 𝑋 ↦ ⟨ [ 𝑘 ] ∼ , ( 𝑘 ⊕ 𝐴 ) ⟩ ) : ( 𝑋 / ∼ ) –1-1-onto→ [ 𝐴 ] 𝑂 )
18	14 17	hasheqf1od	⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑋 ∈ Fin ) → ( ♯ ‘ ( 𝑋 / ∼ ) ) = ( ♯ ‘ [ 𝐴 ] 𝑂 ) )
19	18	oveq1d	⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑋 ∈ Fin ) → ( ( ♯ ‘ ( 𝑋 / ∼ ) ) · ( ♯ ‘ 𝐻 ) ) = ( ( ♯ ‘ [ 𝐴 ] 𝑂 ) · ( ♯ ‘ 𝐻 ) ) )
20	8 19	eqtrd	⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑋 ∈ Fin ) → ( ♯ ‘ 𝑋 ) = ( ( ♯ ‘ [ 𝐴 ] 𝑂 ) · ( ♯ ‘ 𝐻 ) ) )