Theorem odhash

Description: An element of zero order generates an infinite subgroup. (Contributed by Stefan O'Rear, 12-Sep-2015)

	Ref	Expression
Hypotheses	odhash.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
	odhash.o	⊢ 𝑂 = ( od ‘ 𝐺 )
	odhash.k	⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
Assertion	odhash	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( ♯ ‘ ( 𝐾 ‘ { 𝐴 } ) ) = +∞ )

Proof

Step	Hyp	Ref	Expression
1		odhash.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		odhash.o	⊢ 𝑂 = ( od ‘ 𝐺 )
3		odhash.k	⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
4		zex	⊢ ℤ ∈ V
5		ominf	⊢ ¬ ω ∈ Fin
6		znnen	⊢ ℤ ≈ ℕ
7		nnenom	⊢ ℕ ≈ ω
8	6 7	entri	⊢ ℤ ≈ ω
9		enfi	⊢ ( ℤ ≈ ω → ( ℤ ∈ Fin ↔ ω ∈ Fin ) )
10	8 9	ax-mp	⊢ ( ℤ ∈ Fin ↔ ω ∈ Fin )
11	5 10	mtbir	⊢ ¬ ℤ ∈ Fin
12		hashinf	⊢ ( ( ℤ ∈ V ∧ ¬ ℤ ∈ Fin ) → ( ♯ ‘ ℤ ) = +∞ )
13	4 11 12	mp2an	⊢ ( ♯ ‘ ℤ ) = +∞
14		eqid	⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
15	1 14 2 3	odf1o1	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) : ℤ –1-1-onto→ ( 𝐾 ‘ { 𝐴 } ) )
16	4	f1oen	⊢ ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) : ℤ –1-1-onto→ ( 𝐾 ‘ { 𝐴 } ) → ℤ ≈ ( 𝐾 ‘ { 𝐴 } ) )
17		hasheni	⊢ ( ℤ ≈ ( 𝐾 ‘ { 𝐴 } ) → ( ♯ ‘ ℤ ) = ( ♯ ‘ ( 𝐾 ‘ { 𝐴 } ) ) )
18	15 16 17	3syl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( ♯ ‘ ℤ ) = ( ♯ ‘ ( 𝐾 ‘ { 𝐴 } ) ) )
19	13 18	syl5reqr	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( ♯ ‘ ( 𝐾 ‘ { 𝐴 } ) ) = +∞ )