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