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 𝑋 = ( Base ‘ 𝐺 )
odf1.2 𝑂 = ( od ‘ 𝐺 )
odf1.3 · = ( .g𝐺 )
odf1.4 𝐹 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) )
Assertion odinf ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ∧ ( 𝑂𝐴 ) = 0 ) → ¬ ran 𝐹 ∈ Fin )

Proof

Step Hyp Ref Expression
1 odf1.1 𝑋 = ( Base ‘ 𝐺 )
2 odf1.2 𝑂 = ( od ‘ 𝐺 )
3 odf1.3 · = ( .g𝐺 )
4 odf1.4 𝐹 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) )
5 znnen ℤ ≈ ℕ
6 nnenom ℕ ≈ ω
7 5 6 entr2i ω ≈ ℤ
8 1 2 3 4 odf1 ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) → ( ( 𝑂𝐴 ) = 0 ↔ 𝐹 : ℤ –1-1𝑋 ) )
9 8 biimp3a ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ∧ ( 𝑂𝐴 ) = 0 ) → 𝐹 : ℤ –1-1𝑋 )
10 f1f ( 𝐹 : ℤ –1-1𝑋𝐹 : ℤ ⟶ 𝑋 )
11 zex ℤ ∈ V
12 1 fvexi 𝑋 ∈ V
13 fex2 ( ( 𝐹 : ℤ ⟶ 𝑋 ∧ ℤ ∈ V ∧ 𝑋 ∈ V ) → 𝐹 ∈ V )
14 11 12 13 mp3an23 ( 𝐹 : ℤ ⟶ 𝑋𝐹 ∈ V )
15 9 10 14 3syl ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ∧ ( 𝑂𝐴 ) = 0 ) → 𝐹 ∈ V )
16 f1f1orn ( 𝐹 : ℤ –1-1𝑋𝐹 : ℤ –1-1-onto→ ran 𝐹 )
17 9 16 syl ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ∧ ( 𝑂𝐴 ) = 0 ) → 𝐹 : ℤ –1-1-onto→ ran 𝐹 )
18 f1oen3g ( ( 𝐹 ∈ V ∧ 𝐹 : ℤ –1-1-onto→ ran 𝐹 ) → ℤ ≈ ran 𝐹 )
19 15 17 18 syl2anc ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ∧ ( 𝑂𝐴 ) = 0 ) → ℤ ≈ ran 𝐹 )
20 entr ( ( ω ≈ ℤ ∧ ℤ ≈ ran 𝐹 ) → ω ≈ ran 𝐹 )
21 7 19 20 sylancr ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ∧ ( 𝑂𝐴 ) = 0 ) → ω ≈ ran 𝐹 )
22 endom ( ω ≈ ran 𝐹 → ω ≼ ran 𝐹 )
23 domnsym ( ω ≼ ran 𝐹 → ¬ ran 𝐹 ≺ ω )
24 21 22 23 3syl ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ∧ ( 𝑂𝐴 ) = 0 ) → ¬ ran 𝐹 ≺ ω )
25 isfinite ( ran 𝐹 ∈ Fin ↔ ran 𝐹 ≺ ω )
26 24 25 sylnibr ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ∧ ( 𝑂𝐴 ) = 0 ) → ¬ ran 𝐹 ∈ Fin )