Metamath Proof Explorer


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 7 9 sylib ( ( ( ∈ ( 𝐺 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 ) → ( ♯ ‘ 𝑋 ) = ( ( ♯ ‘ [ 𝐴 ] 𝑂 ) · ( ♯ ‘ 𝐻 ) ) )