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		eqid	⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
5	1 4 2 3	odf1o1	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) : ℤ –1-1-onto→ ( 𝐾 ‘ { 𝐴 } ) )
6		zex	⊢ ℤ ∈ V
7	6	f1oen	⊢ ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) : ℤ –1-1-onto→ ( 𝐾 ‘ { 𝐴 } ) → ℤ ≈ ( 𝐾 ‘ { 𝐴 } ) )
8		hasheni	⊢ ( ℤ ≈ ( 𝐾 ‘ { 𝐴 } ) → ( ♯ ‘ ℤ ) = ( ♯ ‘ ( 𝐾 ‘ { 𝐴 } ) ) )
9	5 7 8	3syl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( ♯ ‘ ℤ ) = ( ♯ ‘ ( 𝐾 ‘ { 𝐴 } ) ) )
10		ominf	⊢ ¬ ω ∈ Fin
11		znnen	⊢ ℤ ≈ ℕ
12		nnenom	⊢ ℕ ≈ ω
13	11 12	entri	⊢ ℤ ≈ ω
14		enfi	⊢ ( ℤ ≈ ω → ( ℤ ∈ Fin ↔ ω ∈ Fin ) )
15	13 14	ax-mp	⊢ ( ℤ ∈ Fin ↔ ω ∈ Fin )
16	10 15	mtbir	⊢ ¬ ℤ ∈ Fin
17		hashinf	⊢ ( ( ℤ ∈ V ∧ ¬ ℤ ∈ Fin ) → ( ♯ ‘ ℤ ) = +∞ )
18	6 16 17	mp2an	⊢ ( ♯ ‘ ℤ ) = +∞
19	9 18	eqtr3di	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( ♯ ‘ ( 𝐾 ‘ { 𝐴 } ) ) = +∞ )