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→ ( 𝐾 ‘ { 𝐴 } ) )