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 )