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	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
		iscyg3.e	$⊢ E = \{x \in B \| ran (n \in ℤ ⟼ n \underset{˙}{\cdot} x) = B\}$
		cyggenod.o	$⊢ O = od (G)$
	Assertion	cyggenod2	$⊢ (G \in Grp \land X \in E) \to O (X) = if (B \in Fin, \|B\|, 0)$

Proof

Step	Hyp	Ref	Expression
1		iscyg.1	$⊢ B = {Base}_{G}$
2		iscyg.2	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		iscyg3.e	$⊢ E = \{x \in B \| ran (n \in ℤ ⟼ n \underset{˙}{\cdot} x) = B\}$
4		cyggenod.o	$⊢ O = od (G)$
5	1 2 3	iscyggen	$⊢ X \in E \leftrightarrow (X \in B \land ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) = B)$
6	5	simplbi	$⊢ X \in E \to X \in B$
7		eqid	$⊢ (n \in ℤ ⟼ n \underset{˙}{\cdot} X) = (n \in ℤ ⟼ n \underset{˙}{\cdot} X)$
8	1 4 2 7	dfod2	$⊢ (G \in Grp \land X \in B) \to O (X) = if (ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) \in Fin, \|ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X)\|, 0)$
9	6 8	sylan2	$⊢ (G \in Grp \land X \in E) \to O (X) = if (ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) \in Fin, \|ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X)\|, 0)$
10	5	simprbi	$⊢ X \in E \to ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) = B$
11	10	adantl	$⊢ (G \in Grp \land X \in E) \to ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) = B$
12	11	eleq1d	$⊢ (G \in Grp \land X \in E) \to (ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) \in Fin \leftrightarrow B \in Fin)$
13	11	fveq2d	$⊢ (G \in Grp \land X \in E) \to \|ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X)\| = \|B\|$
14	12 13	ifbieq1d	$⊢ (G \in Grp \land X \in E) \to if (ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) \in Fin, \|ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X)\|, 0) = if (B \in Fin, \|B\|, 0)$
15	9 14	eqtrd	$⊢ (G \in Grp \land X \in E) \to O (X) = if (B \in Fin, \|B\|, 0)$