Theorem 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	⊢ 𝑋 = ( Base ‘ 𝐺 )
	odf1.2	⊢ 𝑂 = ( od ‘ 𝐺 )
	odf1.3	⊢ · = ( .g ‘ 𝐺 )
	odf1.4	⊢ 𝐹 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) )
Assertion	odf1	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑂 ‘ 𝐴 ) = 0 ↔ 𝐹 : ℤ –1-1→ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		odf1.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		odf1.2	⊢ 𝑂 = ( od ‘ 𝐺 )
3		odf1.3	⊢ · = ( .g ‘ 𝐺 )
4		odf1.4	⊢ 𝐹 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) )
5	1 3	mulgcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ℤ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑥 · 𝐴 ) ∈ 𝑋 )
6	5	3expa	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ℤ ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝑥 · 𝐴 ) ∈ 𝑋 )
7	6	an32s	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 · 𝐴 ) ∈ 𝑋 )
8	7 4	fmptd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → 𝐹 : ℤ ⟶ 𝑋 )
9	8	adantr	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → 𝐹 : ℤ ⟶ 𝑋 )
10		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 · 𝐴 ) = ( 𝑦 · 𝐴 ) )
11		ovex	⊢ ( 𝑥 · 𝐴 ) ∈ V
12	10 4 11	fvmpt3i	⊢ ( 𝑦 ∈ ℤ → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 · 𝐴 ) )
13		oveq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 · 𝐴 ) = ( 𝑧 · 𝐴 ) )
14	13 4 11	fvmpt3i	⊢ ( 𝑧 ∈ ℤ → ( 𝐹 ‘ 𝑧 ) = ( 𝑧 · 𝐴 ) )
15	12 14	eqeqan12d	⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ ( 𝑦 · 𝐴 ) = ( 𝑧 · 𝐴 ) ) )
16	15	adantl	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ ( 𝑦 · 𝐴 ) = ( 𝑧 · 𝐴 ) ) )
17		simplr	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( 𝑂 ‘ 𝐴 ) = 0 )
18	17	breq1d	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑦 − 𝑧 ) ↔ 0 ∥ ( 𝑦 − 𝑧 ) ) )
19		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
20	1 2 3 19	odcong	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑦 − 𝑧 ) ↔ ( 𝑦 · 𝐴 ) = ( 𝑧 · 𝐴 ) ) )
21	20	ad4ant124	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑦 − 𝑧 ) ↔ ( 𝑦 · 𝐴 ) = ( 𝑧 · 𝐴 ) ) )
22		zsubcl	⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( 𝑦 − 𝑧 ) ∈ ℤ )
23	22	adantl	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( 𝑦 − 𝑧 ) ∈ ℤ )
24		0dvds	⊢ ( ( 𝑦 − 𝑧 ) ∈ ℤ → ( 0 ∥ ( 𝑦 − 𝑧 ) ↔ ( 𝑦 − 𝑧 ) = 0 ) )
25	23 24	syl	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( 0 ∥ ( 𝑦 − 𝑧 ) ↔ ( 𝑦 − 𝑧 ) = 0 ) )
26	18 21 25	3bitr3d	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( ( 𝑦 · 𝐴 ) = ( 𝑧 · 𝐴 ) ↔ ( 𝑦 − 𝑧 ) = 0 ) )
27		zcn	⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ )
28		zcn	⊢ ( 𝑧 ∈ ℤ → 𝑧 ∈ ℂ )
29		subeq0	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑦 − 𝑧 ) = 0 ↔ 𝑦 = 𝑧 ) )
30	27 28 29	syl2an	⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( ( 𝑦 − 𝑧 ) = 0 ↔ 𝑦 = 𝑧 ) )
31	30	adantl	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( ( 𝑦 − 𝑧 ) = 0 ↔ 𝑦 = 𝑧 ) )
32	16 26 31	3bitrd	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ 𝑦 = 𝑧 ) )
33	32	biimpd	⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
34	33	ralrimivva	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ∀ 𝑦 ∈ ℤ ∀ 𝑧 ∈ ℤ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
35		dff13	⊢ ( 𝐹 : ℤ –1-1→ 𝑋 ↔ ( 𝐹 : ℤ ⟶ 𝑋 ∧ ∀ 𝑦 ∈ ℤ ∀ 𝑧 ∈ ℤ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) ) )
36	9 34 35	sylanbrc	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → 𝐹 : ℤ –1-1→ 𝑋 )
37	1 2 3 19	odid	⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = ( 0g ‘ 𝐺 ) )
38	1 19 3	mulg0	⊢ ( 𝐴 ∈ 𝑋 → ( 0 · 𝐴 ) = ( 0g ‘ 𝐺 ) )
39	37 38	eqtr4d	⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = ( 0 · 𝐴 ) )
40	39	ad2antlr	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : ℤ –1-1→ 𝑋 ) → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = ( 0 · 𝐴 ) )
41	1 2	odcl	⊢ ( 𝐴 ∈ 𝑋 → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
42	41	ad2antlr	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : ℤ –1-1→ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
43	42	nn0zd	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : ℤ –1-1→ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) ∈ ℤ )
44		oveq1	⊢ ( 𝑥 = ( 𝑂 ‘ 𝐴 ) → ( 𝑥 · 𝐴 ) = ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) )
45	44 4 11	fvmpt3i	⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ℤ → ( 𝐹 ‘ ( 𝑂 ‘ 𝐴 ) ) = ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) )
46	43 45	syl	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : ℤ –1-1→ 𝑋 ) → ( 𝐹 ‘ ( 𝑂 ‘ 𝐴 ) ) = ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) )
47		0zd	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : ℤ –1-1→ 𝑋 ) → 0 ∈ ℤ )
48		oveq1	⊢ ( 𝑥 = 0 → ( 𝑥 · 𝐴 ) = ( 0 · 𝐴 ) )
49	48 4 11	fvmpt3i	⊢ ( 0 ∈ ℤ → ( 𝐹 ‘ 0 ) = ( 0 · 𝐴 ) )
50	47 49	syl	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : ℤ –1-1→ 𝑋 ) → ( 𝐹 ‘ 0 ) = ( 0 · 𝐴 ) )
51	40 46 50	3eqtr4d	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : ℤ –1-1→ 𝑋 ) → ( 𝐹 ‘ ( 𝑂 ‘ 𝐴 ) ) = ( 𝐹 ‘ 0 ) )
52		simpr	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : ℤ –1-1→ 𝑋 ) → 𝐹 : ℤ –1-1→ 𝑋 )
53		f1fveq	⊢ ( ( 𝐹 : ℤ –1-1→ 𝑋 ∧ ( ( 𝑂 ‘ 𝐴 ) ∈ ℤ ∧ 0 ∈ ℤ ) ) → ( ( 𝐹 ‘ ( 𝑂 ‘ 𝐴 ) ) = ( 𝐹 ‘ 0 ) ↔ ( 𝑂 ‘ 𝐴 ) = 0 ) )
54	52 43 47 53	syl12anc	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : ℤ –1-1→ 𝑋 ) → ( ( 𝐹 ‘ ( 𝑂 ‘ 𝐴 ) ) = ( 𝐹 ‘ 0 ) ↔ ( 𝑂 ‘ 𝐴 ) = 0 ) )
55	51 54	mpbid	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : ℤ –1-1→ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) = 0 )
56	36 55	impbida	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑂 ‘ 𝐴 ) = 0 ↔ 𝐹 : ℤ –1-1→ 𝑋 ) )