Metamath Proof Explorer


Theorem odhash2

Description: If an element has nonzero order, it generates a subgroup with size equal to the order. (Contributed by Stefan O'Rear, 12-Sep-2015)

Ref Expression
Hypotheses odhash.x
|- X = ( Base ` G )
odhash.o
|- O = ( od ` G )
odhash.k
|- K = ( mrCls ` ( SubGrp ` G ) )
Assertion odhash2
|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) e. NN ) -> ( # ` ( K ` { A } ) ) = ( O ` A ) )

Proof

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