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