Metamath Proof Explorer

Theorem odinf

Description: The multiples of an element with infinite order form an infinite cyclic subgroup of G . (Contributed by Mario Carneiro, 14-Jan-2015)

Ref Expression
Hypotheses odf1.1 
|- X = ( Base ` G )
odf1.2 
|- O = ( od ` G )
odf1.3 
|- .x. = ( .g ` G )
odf1.4 
|- F = ( x e. ZZ |-> ( x .x. A ) )
Assertion odinf 
|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> -. ran F e. Fin )

Proof

Step Hyp Ref Expression
1 odf1.1 
 |-  X = ( Base ` G )
2 odf1.2 
 |-  O = ( od ` G )
3 odf1.3 
 |-  .x. = ( .g ` G )
4 odf1.4 
 |-  F = ( x e. ZZ |-> ( x .x. A ) )
5 znnen 
 |-  ZZ ~~ NN
6 nnenom 
 |-  NN ~~ _om
7 5 6 entr2i 
 |-  _om ~~ ZZ
8 1 2 3 4 odf1 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( O ` A ) = 0 <-> F : ZZ -1-1-> X ) )
9 8 biimp3a 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> F : ZZ -1-1-> X )
10 f1f 
 |-  ( F : ZZ -1-1-> X -> F : ZZ --> X )
11 zex 
 |-  ZZ e. _V
12 1 fvexi 
 |-  X e. _V
13 fex2 
 |-  ( ( F : ZZ --> X /\ ZZ e. _V /\ X e. _V ) -> F e. _V )
14 11 12 13 mp3an23 
 |-  ( F : ZZ --> X -> F e. _V )
15 9 10 14 3syl 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> F e. _V )
16 f1f1orn 
 |-  ( F : ZZ -1-1-> X -> F : ZZ -1-1-onto-> ran F )
17 9 16 syl 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> F : ZZ -1-1-onto-> ran F )
18 f1oen3g 
 |-  ( ( F e. _V /\ F : ZZ -1-1-onto-> ran F ) -> ZZ ~~ ran F )
19 15 17 18 syl2anc 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ZZ ~~ ran F )
20 entr 
 |-  ( ( _om ~~ ZZ /\ ZZ ~~ ran F ) -> _om ~~ ran F )
21 7 19 20 sylancr 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> _om ~~ ran F )
22 endom 
 |-  ( _om ~~ ran F -> _om ~<_ ran F )
23 domnsym 
 |-  ( _om ~<_ ran F -> -. ran F ~< _om )
24 21 22 23 3syl 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> -. ran F ~< _om )
25 isfinite 
 |-  ( ran F e. Fin <-> ran F ~< _om )
26 24 25 sylnibr 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> -. ran F e. Fin )