Metamath Proof Explorer

Theorem odhash

Description: An element of zero order generates an infinite subgroup. (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 odhash 
|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ( # ` ( K ` { A } ) ) = +oo )

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 odf1o1 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ( x e. ZZ |-> ( x ( .g ` G ) A ) ) : ZZ -1-1-onto-> ( K ` { A } ) )
6 zex 
 |-  ZZ e. _V
7 6 f1oen 
 |-  ( ( x e. ZZ |-> ( x ( .g ` G ) A ) ) : ZZ -1-1-onto-> ( K ` { A } ) -> ZZ ~~ ( K ` { A } ) )
8 hasheni 
 |-  ( ZZ ~~ ( K ` { A } ) -> ( # ` ZZ ) = ( # ` ( K ` { A } ) ) )
9 5 7 8 3syl 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ( # ` ZZ ) = ( # ` ( K ` { A } ) ) )
10 ominf 
 |-  -. _om e. Fin
11 znnen 
 |-  ZZ ~~ NN
12 nnenom 
 |-  NN ~~ _om
13 11 12 entri 
 |-  ZZ ~~ _om
14 enfi 
 |-  ( ZZ ~~ _om -> ( ZZ e. Fin <-> _om e. Fin ) )
15 13 14 ax-mp 
 |-  ( ZZ e. Fin <-> _om e. Fin )
16 10 15 mtbir 
 |-  -. ZZ e. Fin
17 hashinf 
 |-  ( ( ZZ e. _V /\ -. ZZ e. Fin ) -> ( # ` ZZ ) = +oo )
18 6 16 17 mp2an 
 |-  ( # ` ZZ ) = +oo
19 9 18 eqtr3di 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ( # ` ( K ` { A } ) ) = +oo )