odinf

Description: The multiples of an element with infinite order form an infinite cyclic subgroup of G . (Contributed by Mario Carneiro, 14-Jan-2015)

	Ref	Expression
Hypotheses	odf1.1	$⊢ X = {Base}_{G}$
	odf1.2	$⊢ O = od (G)$
	odf1.3	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	odf1.4	$⊢ F = (x \in ℤ ⟼ x \underset{˙}{\cdot} A)$
Assertion	odinf	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to \neg ran F \in Fin$

Proof

Step	Hyp	Ref	Expression
1		odf1.1	$⊢ X = {Base}_{G}$
2		odf1.2	$⊢ O = od (G)$
3		odf1.3	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
4		odf1.4	$⊢ F = (x \in ℤ ⟼ x \underset{˙}{\cdot} A)$
5		znnen	$⊢ ℤ \approx ℕ$
6		nnenom	$⊢ ℕ \approx ω$
7	5 6	entr2i	$⊢ ω \approx ℤ$
8	1 2 3 4	odf1	$⊢ (G \in Grp \land A \in X) \to (O (A) = 0 \leftrightarrow F : ℤ \underset{1-1}{⟶} X)$
9	8	biimp3a	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to F : ℤ \underset{1-1}{⟶} X$
10		f1f	$⊢ F : ℤ \underset{1-1}{⟶} X \to F : ℤ ⟶ X$
11		zex	$⊢ ℤ \in V$
12	1	fvexi	$⊢ X \in V$
13		fex2	$⊢ (F : ℤ ⟶ X \land ℤ \in V \land X \in V) \to F \in V$
14	11 12 13	mp3an23	$⊢ F : ℤ ⟶ X \to F \in V$
15	9 10 14	3syl	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to F \in V$
16		f1f1orn	$⊢ F : ℤ \underset{1-1}{⟶} X \to F : ℤ \underset{1-1 onto}{⟶} ran F$
17	9 16	syl	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to F : ℤ \underset{1-1 onto}{⟶} ran F$
18		f1oen3g	$⊢ (F \in V \land F : ℤ \underset{1-1 onto}{⟶} ran F) \to ℤ \approx ran F$
19	15 17 18	syl2anc	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to ℤ \approx ran F$
20		entr	$⊢ (ω \approx ℤ \land ℤ \approx ran F) \to ω \approx ran F$
21	7 19 20	sylancr	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to ω \approx ran F$
22		endom	$⊢ ω \approx ran F \to ω ≼ ran F$
23		domnsym	$⊢ ω ≼ ran F \to \neg ran F ≺ ω$
24	21 22 23	3syl	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to \neg ran F ≺ ω$
25		isfinite	$⊢ ran F \in Fin \leftrightarrow ran F ≺ ω$
26	24 25	sylnibr	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to \neg ran F \in Fin$

Metamath Proof Explorer

Theorem odinf

Proof