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 ) ) )