odhash

Description: An element of zero order generates an infinite subgroup. (Contributed by Stefan O'Rear, 12-Sep-2015)

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	$⊢ \cdot_{G} = \cdot_{G}$
5	1 4 2 3	odf1o1	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to (x \in ℤ ⟼ x \cdot_{G} A) : ℤ \underset{1-1 onto}{⟶} K (\{A\})$
6		zex	$⊢ ℤ \in V$
7	6	f1oen	$⊢ (x \in ℤ ⟼ x \cdot_{G} A) : ℤ \underset{1-1 onto}{⟶} K (\{A\}) \to ℤ \approx K (\{A\})$
8		hasheni	$⊢ ℤ \approx K (\{A\}) \to \|ℤ\| = \|K (\{A\})\|$
9	5 7 8	3syl	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to \|ℤ\| = \|K (\{A\})\|$
10		ominf	$⊢ \neg ω \in Fin$
11		znnen	$⊢ ℤ \approx ℕ$
12		nnenom	$⊢ ℕ \approx ω$
13	11 12	entri	$⊢ ℤ \approx ω$
14		enfi	$⊢ ℤ \approx ω \to (ℤ \in Fin \leftrightarrow ω \in Fin)$
15	13 14	ax-mp	$⊢ ℤ \in Fin \leftrightarrow ω \in Fin$
16	10 15	mtbir	$⊢ \neg ℤ \in Fin$
17		hashinf	$⊢ (ℤ \in V \land \neg ℤ \in Fin) \to \|ℤ\| = +∞$
18	6 16 17	mp2an	$⊢ \|ℤ\| = +∞$
19	9 18	eqtr3di	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to \|K (\{A\})\| = +∞$

Metamath Proof Explorer