Metamath Proof Explorer

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 ⊢ X = Base G
odhash.o ⊢ O = od ⁡ G
odhash.k ⊢ K = mrCls ⁡ SubGrp ⁡ G
Assertion odhash ⊢ G ∈ Grp ∧ A ∈ X ∧ O ⁡ A = 0 → K ⁡ A = +∞

Proof

Step Hyp Ref Expression
1 odhash.x ⊢ X = Base G
2 odhash.o ⊢ O = od ⁡ G
3 odhash.k ⊢ K = mrCls ⁡ SubGrp ⁡ G
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 ⊢ G ∈ Grp ∧ A ∈ X ∧ O ⁡ A = 0 → x ∈ ℤ ⟼ x ⋅ G A : ℤ ⟶ 1-1 onto K ⁡ A
16 4 f1oen ⊢ x ∈ ℤ ⟼ x ⋅ G A : ℤ ⟶ 1-1 onto K ⁡ A → ℤ ≈ K ⁡ A
17 hasheni ⊢ ℤ ≈ K ⁡ A → ℤ = K ⁡ A
18 15 16 17 3syl ⊢ G ∈ Grp ∧ A ∈ X ∧ O ⁡ A = 0 → ℤ = K ⁡ A
19 13 18 syl5reqr ⊢ G ∈ Grp ∧ A ∈ X ∧ O ⁡ A = 0 → K ⁡ A = +∞