Metamath Proof Explorer

Theorem odf1o1

Description: An element with zero order has infinitely many multiples. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Hypotheses odf1o1.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
odf1o1.t ⊢ · = ( .g ‘ 𝐺 )
odf1o1.o ⊢ 𝑂 = ( od ‘ 𝐺 )
odf1o1.k ⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
Assertion odf1o1 ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) : ℤ –1-1-onto→ ( 𝐾 ‘ { 𝐴 } ) )

Proof

Step Hyp Ref Expression
1 odf1o1.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 odf1o1.t ⊢ · = ( .g ‘ 𝐺 )
3 odf1o1.o ⊢ 𝑂 = ( od ‘ 𝐺 )
4 odf1o1.k ⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
5 simpl1 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ 𝑥 ∈ ℤ ) → 𝐺 ∈ Grp )
6 1 subgacs ⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝑋 ) )
7 acsmre ⊢ ( ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝑋 ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝑋 ) )
8 5 6 7 3syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ 𝑥 ∈ ℤ ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝑋 ) )
9 simpl2 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ 𝑥 ∈ ℤ ) → 𝐴 ∈ 𝑋 )
10 9 snssd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ 𝑥 ∈ ℤ ) → { 𝐴 } ⊆ 𝑋 )
11 4 mrccl ⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝑋 ) ∧ { 𝐴 } ⊆ 𝑋 ) → ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) )
12 8 10 11 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ 𝑥 ∈ ℤ ) → ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) )
13 simpr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ 𝑥 ∈ ℤ ) → 𝑥 ∈ ℤ )
14 8 4 10 mrcssidd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ 𝑥 ∈ ℤ ) → { 𝐴 } ⊆ ( 𝐾 ‘ { 𝐴 } ) )
15 snidg ⊢ ( 𝐴 ∈ 𝑋 → 𝐴 ∈ { 𝐴 } )
16 9 15 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ 𝑥 ∈ ℤ ) → 𝐴 ∈ { 𝐴 } )
17 14 16 sseldd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ 𝑥 ∈ ℤ ) → 𝐴 ∈ ( 𝐾 ‘ { 𝐴 } ) )
18 2 subgmulgcl ⊢ ( ( ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ℤ ∧ 𝐴 ∈ ( 𝐾 ‘ { 𝐴 } ) ) → ( 𝑥 · 𝐴 ) ∈ ( 𝐾 ‘ { 𝐴 } ) )
19 12 13 17 18 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 · 𝐴 ) ∈ ( 𝐾 ‘ { 𝐴 } ) )
20 19 ex ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 𝑥 ∈ ℤ → ( 𝑥 · 𝐴 ) ∈ ( 𝐾 ‘ { 𝐴 } ) ) )
21 simpl3 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑂 ‘ 𝐴 ) = 0 )
22 21 breq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑥 − 𝑦 ) ↔ 0 ∥ ( 𝑥 − 𝑦 ) ) )
23 zsubcl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 − 𝑦 ) ∈ ℤ )
24 23 adantl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑥 − 𝑦 ) ∈ ℤ )
25 0dvds ⊢ ( ( 𝑥 − 𝑦 ) ∈ ℤ → ( 0 ∥ ( 𝑥 − 𝑦 ) ↔ ( 𝑥 − 𝑦 ) = 0 ) )
26 24 25 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 0 ∥ ( 𝑥 − 𝑦 ) ↔ ( 𝑥 − 𝑦 ) = 0 ) )
27 22 26 bitrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑥 − 𝑦 ) ↔ ( 𝑥 − 𝑦 ) = 0 ) )
28 simpl1 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝐺 ∈ Grp )
29 simpl2 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝐴 ∈ 𝑋 )
30 simprl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑥 ∈ ℤ )
31 simprr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑦 ∈ ℤ )
32 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
33 1 3 2 32 odcong ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑥 − 𝑦 ) ↔ ( 𝑥 · 𝐴 ) = ( 𝑦 · 𝐴 ) ) )
34 28 29 30 31 33 syl112anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑥 − 𝑦 ) ↔ ( 𝑥 · 𝐴 ) = ( 𝑦 · 𝐴 ) ) )
35 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
36 zcn ⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ )
37 subeq0 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑥 − 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
38 35 36 37 syl2an ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑥 − 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
39 38 adantl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑥 − 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
40 27 34 39 3bitr3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑥 · 𝐴 ) = ( 𝑦 · 𝐴 ) ↔ 𝑥 = 𝑦 ) )
41 40 ex ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑥 · 𝐴 ) = ( 𝑦 · 𝐴 ) ↔ 𝑥 = 𝑦 ) ) )
42 20 41 dom2lem ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) : ℤ –1-1→ ( 𝐾 ‘ { 𝐴 } ) )
43 19 fmpttd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) : ℤ ⟶ ( 𝐾 ‘ { 𝐴 } ) )
44 eqid ⊢ ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) = ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) )
45 1 2 44 4 cycsubg2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐾 ‘ { 𝐴 } ) = ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) )
46 45 3adant3 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 𝐾 ‘ { 𝐴 } ) = ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) )
47 46 eqcomd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) = ( 𝐾 ‘ { 𝐴 } ) )
48 dffo2 ⊢ ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) : ℤ –onto→ ( 𝐾 ‘ { 𝐴 } ) ↔ ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) : ℤ ⟶ ( 𝐾 ‘ { 𝐴 } ) ∧ ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) = ( 𝐾 ‘ { 𝐴 } ) ) )
49 43 47 48 sylanbrc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) : ℤ –onto→ ( 𝐾 ‘ { 𝐴 } ) )
50 df-f1o ⊢ ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) : ℤ –1-1-onto→ ( 𝐾 ‘ { 𝐴 } ) ↔ ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) : ℤ –1-1→ ( 𝐾 ‘ { 𝐴 } ) ∧ ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) : ℤ –onto→ ( 𝐾 ‘ { 𝐴 } ) ) )
51 42 49 50 sylanbrc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) : ℤ –1-1-onto→ ( 𝐾 ‘ { 𝐴 } ) )