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
|- X = ( Base ` G )
orbsta2.h
|- H = { u e. X | ( u .(+) A ) = A }
orbsta2.r
|- .~ = ( G ~QG H )
orbsta2.o
|- O = { <. x , y >. | ( { x , y } C_ Y /\ E. g e. X ( g .(+) x ) = y ) }
Assertion orbsta2
|- ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ X e. Fin ) -> ( # ` X ) = ( ( # ` [ A ] O ) x. ( # ` H ) ) )

Proof

Step Hyp Ref Expression
1 orbsta2.x
 |-  X = ( Base ` G )
2 orbsta2.h
 |-  H = { u e. X | ( u .(+) A ) = A }
3 orbsta2.r
 |-  .~ = ( G ~QG H )
4 orbsta2.o
 |-  O = { <. x , y >. | ( { x , y } C_ Y /\ E. g e. X ( g .(+) x ) = y ) }
5 1 2 gastacl
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> H e. ( SubGrp ` G ) )
6 5 adantr
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ X e. Fin ) -> H e. ( SubGrp ` G ) )
7 simpr
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ X e. Fin ) -> X e. Fin )
8 1 3 6 7 lagsubg2
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ X e. Fin ) -> ( # ` X ) = ( ( # ` ( X /. .~ ) ) x. ( # ` H ) ) )
9 pwfi
 |-  ( X e. Fin <-> ~P X e. Fin )
10 7 9 sylib
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ X e. Fin ) -> ~P X e. Fin )
11 1 3 eqger
 |-  ( H e. ( SubGrp ` G ) -> .~ Er X )
12 6 11 syl
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ X e. Fin ) -> .~ Er X )
13 12 qsss
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ X e. Fin ) -> ( X /. .~ ) C_ ~P X )
14 10 13 ssfid
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ X e. Fin ) -> ( X /. .~ ) e. Fin )
15 eqid
 |-  ran ( k e. X |-> <. [ k ] .~ , ( k .(+) A ) >. ) = ran ( k e. X |-> <. [ k ] .~ , ( k .(+) A ) >. )
16 1 2 3 15 4 orbsta
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> ran ( k e. X |-> <. [ k ] .~ , ( k .(+) A ) >. ) : ( X /. .~ ) -1-1-onto-> [ A ] O )
17 16 adantr
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ X e. Fin ) -> ran ( k e. X |-> <. [ k ] .~ , ( k .(+) A ) >. ) : ( X /. .~ ) -1-1-onto-> [ A ] O )
18 14 17 hasheqf1od
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ X e. Fin ) -> ( # ` ( X /. .~ ) ) = ( # ` [ A ] O ) )
19 18 oveq1d
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ X e. Fin ) -> ( ( # ` ( X /. .~ ) ) x. ( # ` H ) ) = ( ( # ` [ A ] O ) x. ( # ` H ) ) )
20 8 19 eqtrd
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ X e. Fin ) -> ( # ` X ) = ( ( # ` [ A ] O ) x. ( # ` H ) ) )