This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )