odf1

Description: The multiples of an element with infinite order form an infinite cyclic subgroup of G . (Contributed by Mario Carneiro, 14-Jan-2015) (Revised by Mario Carneiro, 23-Sep-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	odf1	$⊢ (G \in Grp \land A \in X) \to (O (A) = 0 \leftrightarrow F : ℤ \underset{1-1}{⟶} X)$

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	1 3	mulgcl	$⊢ (G \in Grp \land x \in ℤ \land A \in X) \to x \underset{˙}{\cdot} A \in X$
6	5	3expa	$⊢ ((G \in Grp \land x \in ℤ) \land A \in X) \to x \underset{˙}{\cdot} A \in X$
7	6	an32s	$⊢ ((G \in Grp \land A \in X) \land x \in ℤ) \to x \underset{˙}{\cdot} A \in X$
8	7 4	fmptd	$⊢ (G \in Grp \land A \in X) \to F : ℤ ⟶ X$
9	8	adantr	$⊢ ((G \in Grp \land A \in X) \land O (A) = 0) \to F : ℤ ⟶ X$
10		oveq1	$⊢ x = y \to x \underset{˙}{\cdot} A = y \underset{˙}{\cdot} A$
11		ovex	$⊢ x \underset{˙}{\cdot} A \in V$
12	10 4 11	fvmpt3i	$⊢ y \in ℤ \to F (y) = y \underset{˙}{\cdot} A$
13		oveq1	$⊢ x = z \to x \underset{˙}{\cdot} A = z \underset{˙}{\cdot} A$
14	13 4 11	fvmpt3i	$⊢ z \in ℤ \to F (z) = z \underset{˙}{\cdot} A$
15	12 14	eqeqan12d	$⊢ (y \in ℤ \land z \in ℤ) \to (F (y) = F (z) \leftrightarrow y \underset{˙}{\cdot} A = z \underset{˙}{\cdot} A)$
16	15	adantl	$⊢ (((G \in Grp \land A \in X) \land O (A) = 0) \land (y \in ℤ \land z \in ℤ)) \to (F (y) = F (z) \leftrightarrow y \underset{˙}{\cdot} A = z \underset{˙}{\cdot} A)$
17		simplr	$⊢ (((G \in Grp \land A \in X) \land O (A) = 0) \land (y \in ℤ \land z \in ℤ)) \to O (A) = 0$
18	17	breq1d	$⊢ (((G \in Grp \land A \in X) \land O (A) = 0) \land (y \in ℤ \land z \in ℤ)) \to (O (A) ∥ (y - z) \leftrightarrow 0 ∥ (y - z))$
19		eqid	$⊢ 0_{G} = 0_{G}$
20	1 2 3 19	odcong	$⊢ (G \in Grp \land A \in X \land (y \in ℤ \land z \in ℤ)) \to (O (A) ∥ (y - z) \leftrightarrow y \underset{˙}{\cdot} A = z \underset{˙}{\cdot} A)$
21	20	ad4ant124	$⊢ (((G \in Grp \land A \in X) \land O (A) = 0) \land (y \in ℤ \land z \in ℤ)) \to (O (A) ∥ (y - z) \leftrightarrow y \underset{˙}{\cdot} A = z \underset{˙}{\cdot} A)$
22		zsubcl	$⊢ (y \in ℤ \land z \in ℤ) \to y - z \in ℤ$
23	22	adantl	$⊢ (((G \in Grp \land A \in X) \land O (A) = 0) \land (y \in ℤ \land z \in ℤ)) \to y - z \in ℤ$
24		0dvds	$⊢ y - z \in ℤ \to (0 ∥ (y - z) \leftrightarrow y - z = 0)$
25	23 24	syl	$⊢ (((G \in Grp \land A \in X) \land O (A) = 0) \land (y \in ℤ \land z \in ℤ)) \to (0 ∥ (y - z) \leftrightarrow y - z = 0)$
26	18 21 25	3bitr3d	$⊢ (((G \in Grp \land A \in X) \land O (A) = 0) \land (y \in ℤ \land z \in ℤ)) \to (y \underset{˙}{\cdot} A = z \underset{˙}{\cdot} A \leftrightarrow y - z = 0)$
27		zcn	$⊢ y \in ℤ \to y \in ℂ$
28		zcn	$⊢ z \in ℤ \to z \in ℂ$
29		subeq0	$⊢ (y \in ℂ \land z \in ℂ) \to (y - z = 0 \leftrightarrow y = z)$
30	27 28 29	syl2an	$⊢ (y \in ℤ \land z \in ℤ) \to (y - z = 0 \leftrightarrow y = z)$
31	30	adantl	$⊢ (((G \in Grp \land A \in X) \land O (A) = 0) \land (y \in ℤ \land z \in ℤ)) \to (y - z = 0 \leftrightarrow y = z)$
32	16 26 31	3bitrd	$⊢ (((G \in Grp \land A \in X) \land O (A) = 0) \land (y \in ℤ \land z \in ℤ)) \to (F (y) = F (z) \leftrightarrow y = z)$
33	32	biimpd	$⊢ (((G \in Grp \land A \in X) \land O (A) = 0) \land (y \in ℤ \land z \in ℤ)) \to (F (y) = F (z) \to y = z)$
34	33	ralrimivva	$⊢ ((G \in Grp \land A \in X) \land O (A) = 0) \to \forall y \in ℤ \forall z \in ℤ (F (y) = F (z) \to y = z)$
35		dff13	$⊢ F : ℤ \underset{1-1}{⟶} X \leftrightarrow (F : ℤ ⟶ X \land \forall y \in ℤ \forall z \in ℤ (F (y) = F (z) \to y = z))$
36	9 34 35	sylanbrc	$⊢ ((G \in Grp \land A \in X) \land O (A) = 0) \to F : ℤ \underset{1-1}{⟶} X$
37	1 2 3 19	odid	$⊢ A \in X \to O (A) \underset{˙}{\cdot} A = 0_{G}$
38	1 19 3	mulg0	$⊢ A \in X \to 0 \underset{˙}{\cdot} A = 0_{G}$
39	37 38	eqtr4d	$⊢ A \in X \to O (A) \underset{˙}{\cdot} A = 0 \underset{˙}{\cdot} A$
40	39	ad2antlr	$⊢ ((G \in Grp \land A \in X) \land F : ℤ \underset{1-1}{⟶} X) \to O (A) \underset{˙}{\cdot} A = 0 \underset{˙}{\cdot} A$
41	1 2	odcl	$⊢ A \in X \to O (A) \in ℕ_{0}$
42	41	ad2antlr	$⊢ ((G \in Grp \land A \in X) \land F : ℤ \underset{1-1}{⟶} X) \to O (A) \in ℕ_{0}$
43	42	nn0zd	$⊢ ((G \in Grp \land A \in X) \land F : ℤ \underset{1-1}{⟶} X) \to O (A) \in ℤ$
44		oveq1	$⊢ x = O (A) \to x \underset{˙}{\cdot} A = O (A) \underset{˙}{\cdot} A$
45	44 4 11	fvmpt3i	$⊢ O (A) \in ℤ \to F (O (A)) = O (A) \underset{˙}{\cdot} A$
46	43 45	syl	$⊢ ((G \in Grp \land A \in X) \land F : ℤ \underset{1-1}{⟶} X) \to F (O (A)) = O (A) \underset{˙}{\cdot} A$
47		0zd	$⊢ ((G \in Grp \land A \in X) \land F : ℤ \underset{1-1}{⟶} X) \to 0 \in ℤ$
48		oveq1	$⊢ x = 0 \to x \underset{˙}{\cdot} A = 0 \underset{˙}{\cdot} A$
49	48 4 11	fvmpt3i	$⊢ 0 \in ℤ \to F (0) = 0 \underset{˙}{\cdot} A$
50	47 49	syl	$⊢ ((G \in Grp \land A \in X) \land F : ℤ \underset{1-1}{⟶} X) \to F (0) = 0 \underset{˙}{\cdot} A$
51	40 46 50	3eqtr4d	$⊢ ((G \in Grp \land A \in X) \land F : ℤ \underset{1-1}{⟶} X) \to F (O (A)) = F (0)$
52		simpr	$⊢ ((G \in Grp \land A \in X) \land F : ℤ \underset{1-1}{⟶} X) \to F : ℤ \underset{1-1}{⟶} X$
53		f1fveq	$⊢ (F : ℤ \underset{1-1}{⟶} X \land (O (A) \in ℤ \land 0 \in ℤ)) \to (F (O (A)) = F (0) \leftrightarrow O (A) = 0)$
54	52 43 47 53	syl12anc	$⊢ ((G \in Grp \land A \in X) \land F : ℤ \underset{1-1}{⟶} X) \to (F (O (A)) = F (0) \leftrightarrow O (A) = 0)$
55	51 54	mpbid	$⊢ ((G \in Grp \land A \in X) \land F : ℤ \underset{1-1}{⟶} X) \to O (A) = 0$
56	36 55	impbida	$⊢ (G \in Grp \land A \in X) \to (O (A) = 0 \leftrightarrow F : ℤ \underset{1-1}{⟶} X)$

Metamath Proof Explorer

Theorem odf1

Proof