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 eqid ⊢ ⋅ G = ⋅ G
5 1 4 2 3 odf1o1 ⊢ G ∈ Grp ∧ A ∈ X ∧ O ⁡ A = 0 → x ∈ ℤ ⟼ x ⋅ G A : ℤ ⟶ 1-1 onto K ⁡ A
6 zex ⊢ ℤ ∈ V
7 6 f1oen ⊢ x ∈ ℤ ⟼ x ⋅ G A : ℤ ⟶ 1-1 onto K ⁡ A → ℤ ≈ K ⁡ A
8 hasheni ⊢ ℤ ≈ K ⁡ A → ℤ = K ⁡ A
9 5 7 8 3syl ⊢ G ∈ Grp ∧ A ∈ X ∧ O ⁡ A = 0 → ℤ = K ⁡ A
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 ⊢ G ∈ Grp ∧ A ∈ X ∧ O ⁡ A = 0 → K ⁡ A = +∞