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 )