This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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→ 𝑋 ) )