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