Metamath Proof Explorer

Theorem cyggenod2

Description: In an infinite cyclic group, the generator must have infinite order, but this property no longer characterizes the generators. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses iscyg.1 ⊢ B = Base G
iscyg.2 ⊢ · ˙ = ⋅ G
iscyg3.e ⊢ E = x ∈ B | ran ⁡ n ∈ ℤ ⟼ n · ˙ x = B
cyggenod.o ⊢ O = od ⁡ G
Assertion cyggenod2 ⊢ G ∈ Grp ∧ X ∈ E → O ⁡ X = if B ∈ Fin B 0

Proof

Step Hyp Ref Expression
1 iscyg.1 ⊢ B = Base G
2 iscyg.2 ⊢ · ˙ = ⋅ G
3 iscyg3.e ⊢ E = x ∈ B | ran ⁡ n ∈ ℤ ⟼ n · ˙ x = B
4 cyggenod.o ⊢ O = od ⁡ G
5 1 2 3 iscyggen ⊢ X ∈ E ↔ X ∈ B ∧ ran ⁡ n ∈ ℤ ⟼ n · ˙ X = B
6 5 simplbi ⊢ X ∈ E → X ∈ B
7 eqid ⊢ n ∈ ℤ ⟼ n · ˙ X = n ∈ ℤ ⟼ n · ˙ X
8 1 4 2 7 dfod2 ⊢ G ∈ Grp ∧ X ∈ B → O ⁡ X = if ran ⁡ n ∈ ℤ ⟼ n · ˙ X ∈ Fin ran ⁡ n ∈ ℤ ⟼ n · ˙ X 0
9 6 8 sylan2 ⊢ G ∈ Grp ∧ X ∈ E → O ⁡ X = if ran ⁡ n ∈ ℤ ⟼ n · ˙ X ∈ Fin ran ⁡ n ∈ ℤ ⟼ n · ˙ X 0
10 5 simprbi ⊢ X ∈ E → ran ⁡ n ∈ ℤ ⟼ n · ˙ X = B
11 10 adantl ⊢ G ∈ Grp ∧ X ∈ E → ran ⁡ n ∈ ℤ ⟼ n · ˙ X = B
12 11 eleq1d ⊢ G ∈ Grp ∧ X ∈ E → ran ⁡ n ∈ ℤ ⟼ n · ˙ X ∈ Fin ↔ B ∈ Fin
13 11 fveq2d ⊢ G ∈ Grp ∧ X ∈ E → ran ⁡ n ∈ ℤ ⟼ n · ˙ X = B
14 12 13 ifbieq1d ⊢ G ∈ Grp ∧ X ∈ E → if ran ⁡ n ∈ ℤ ⟼ n · ˙ X ∈ Fin ran ⁡ n ∈ ℤ ⟼ n · ˙ X 0 = if B ∈ Fin B 0
15 9 14 eqtrd ⊢ G ∈ Grp ∧ X ∈ E → O ⁡ X = if B ∈ Fin B 0