# 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}={\mathrm{Base}}_{{G}}$
odf1.2 ${⊢}{O}=\mathrm{od}\left({G}\right)$
odf1.3
odf1.4
Assertion odinf ${⊢}\left({G}\in \mathrm{Grp}\wedge {A}\in {X}\wedge {O}\left({A}\right)=0\right)\to ¬\mathrm{ran}{F}\in \mathrm{Fin}$

### Proof

Step Hyp Ref Expression
1 odf1.1 ${⊢}{X}={\mathrm{Base}}_{{G}}$
2 odf1.2 ${⊢}{O}=\mathrm{od}\left({G}\right)$
3 odf1.3
4 odf1.4
5 znnen ${⊢}ℤ\approx ℕ$
6 nnenom ${⊢}ℕ\approx \mathrm{\omega }$
7 5 6 entr2i ${⊢}\mathrm{\omega }\approx ℤ$
8 1 2 3 4 odf1 ${⊢}\left({G}\in \mathrm{Grp}\wedge {A}\in {X}\right)\to \left({O}\left({A}\right)=0↔{F}:ℤ\underset{1-1}{⟶}{X}\right)$
9 8 biimp3a ${⊢}\left({G}\in \mathrm{Grp}\wedge {A}\in {X}\wedge {O}\left({A}\right)=0\right)\to {F}:ℤ\underset{1-1}{⟶}{X}$
10 f1f ${⊢}{F}:ℤ\underset{1-1}{⟶}{X}\to {F}:ℤ⟶{X}$
11 zex ${⊢}ℤ\in \mathrm{V}$
12 1 fvexi ${⊢}{X}\in \mathrm{V}$
13 fex2 ${⊢}\left({F}:ℤ⟶{X}\wedge ℤ\in \mathrm{V}\wedge {X}\in \mathrm{V}\right)\to {F}\in \mathrm{V}$
14 11 12 13 mp3an23 ${⊢}{F}:ℤ⟶{X}\to {F}\in \mathrm{V}$
15 9 10 14 3syl ${⊢}\left({G}\in \mathrm{Grp}\wedge {A}\in {X}\wedge {O}\left({A}\right)=0\right)\to {F}\in \mathrm{V}$
16 f1f1orn ${⊢}{F}:ℤ\underset{1-1}{⟶}{X}\to {F}:ℤ\underset{1-1 onto}{⟶}\mathrm{ran}{F}$
17 9 16 syl ${⊢}\left({G}\in \mathrm{Grp}\wedge {A}\in {X}\wedge {O}\left({A}\right)=0\right)\to {F}:ℤ\underset{1-1 onto}{⟶}\mathrm{ran}{F}$
18 f1oen3g ${⊢}\left({F}\in \mathrm{V}\wedge {F}:ℤ\underset{1-1 onto}{⟶}\mathrm{ran}{F}\right)\to ℤ\approx \mathrm{ran}{F}$
19 15 17 18 syl2anc ${⊢}\left({G}\in \mathrm{Grp}\wedge {A}\in {X}\wedge {O}\left({A}\right)=0\right)\to ℤ\approx \mathrm{ran}{F}$
20 entr ${⊢}\left(\mathrm{\omega }\approx ℤ\wedge ℤ\approx \mathrm{ran}{F}\right)\to \mathrm{\omega }\approx \mathrm{ran}{F}$
21 7 19 20 sylancr ${⊢}\left({G}\in \mathrm{Grp}\wedge {A}\in {X}\wedge {O}\left({A}\right)=0\right)\to \mathrm{\omega }\approx \mathrm{ran}{F}$
22 endom ${⊢}\mathrm{\omega }\approx \mathrm{ran}{F}\to \mathrm{\omega }\preccurlyeq \mathrm{ran}{F}$
23 domnsym ${⊢}\mathrm{\omega }\preccurlyeq \mathrm{ran}{F}\to ¬\mathrm{ran}{F}\prec \mathrm{\omega }$
24 21 22 23 3syl ${⊢}\left({G}\in \mathrm{Grp}\wedge {A}\in {X}\wedge {O}\left({A}\right)=0\right)\to ¬\mathrm{ran}{F}\prec \mathrm{\omega }$
25 isfinite ${⊢}\mathrm{ran}{F}\in \mathrm{Fin}↔\mathrm{ran}{F}\prec \mathrm{\omega }$
26 24 25 sylnibr ${⊢}\left({G}\in \mathrm{Grp}\wedge {A}\in {X}\wedge {O}\left({A}\right)=0\right)\to ¬\mathrm{ran}{F}\in \mathrm{Fin}$