Step |
Hyp |
Ref |
Expression |
1 |
|
odhash.x |
|- X = ( Base ` G ) |
2 |
|
odhash.o |
|- O = ( od ` G ) |
3 |
|
odhash.k |
|- K = ( mrCls ` ( SubGrp ` G ) ) |
4 |
|
eqid |
|- ( .g ` G ) = ( .g ` G ) |
5 |
1 4 2 3
|
odf1o2 |
|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) e. NN ) -> ( x e. ( 0 ..^ ( O ` A ) ) |-> ( x ( .g ` G ) A ) ) : ( 0 ..^ ( O ` A ) ) -1-1-onto-> ( K ` { A } ) ) |
6 |
|
ovex |
|- ( 0 ..^ ( O ` A ) ) e. _V |
7 |
6
|
f1oen |
|- ( ( x e. ( 0 ..^ ( O ` A ) ) |-> ( x ( .g ` G ) A ) ) : ( 0 ..^ ( O ` A ) ) -1-1-onto-> ( K ` { A } ) -> ( 0 ..^ ( O ` A ) ) ~~ ( K ` { A } ) ) |
8 |
|
hasheni |
|- ( ( 0 ..^ ( O ` A ) ) ~~ ( K ` { A } ) -> ( # ` ( 0 ..^ ( O ` A ) ) ) = ( # ` ( K ` { A } ) ) ) |
9 |
5 7 8
|
3syl |
|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) e. NN ) -> ( # ` ( 0 ..^ ( O ` A ) ) ) = ( # ` ( K ` { A } ) ) ) |
10 |
1 2
|
odcl |
|- ( A e. X -> ( O ` A ) e. NN0 ) |
11 |
10
|
3ad2ant2 |
|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) e. NN ) -> ( O ` A ) e. NN0 ) |
12 |
|
hashfzo0 |
|- ( ( O ` A ) e. NN0 -> ( # ` ( 0 ..^ ( O ` A ) ) ) = ( O ` A ) ) |
13 |
11 12
|
syl |
|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) e. NN ) -> ( # ` ( 0 ..^ ( O ` A ) ) ) = ( O ` A ) ) |
14 |
9 13
|
eqtr3d |
|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) e. NN ) -> ( # ` ( K ` { A } ) ) = ( O ` A ) ) |