Metamath Proof Explorer


Theorem cycsubgcyg

Description: The cyclic subgroup generated by A is a cyclic group. (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses cycsubgcyg.x 𝑋 = ( Base ‘ 𝐺 )
cycsubgcyg.t · = ( .g𝐺 )
cycsubgcyg.s 𝑆 = ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) )
Assertion cycsubgcyg ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) → ( 𝐺s 𝑆 ) ∈ CycGrp )

Proof

Step Hyp Ref Expression
1 cycsubgcyg.x 𝑋 = ( Base ‘ 𝐺 )
2 cycsubgcyg.t · = ( .g𝐺 )
3 cycsubgcyg.s 𝑆 = ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) )
4 eqid ( Base ‘ ( 𝐺s 𝑆 ) ) = ( Base ‘ ( 𝐺s 𝑆 ) )
5 eqid ( .g ‘ ( 𝐺s 𝑆 ) ) = ( .g ‘ ( 𝐺s 𝑆 ) )
6 eqid ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) = ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) )
7 1 2 6 cycsubgcl ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) → ( ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) ) )
8 7 simpld ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) → ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) ∈ ( SubGrp ‘ 𝐺 ) )
9 3 8 eqeltrid ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
10 eqid ( 𝐺s 𝑆 ) = ( 𝐺s 𝑆 )
11 10 subggrp ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺s 𝑆 ) ∈ Grp )
12 9 11 syl ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) → ( 𝐺s 𝑆 ) ∈ Grp )
13 7 simprd ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) → 𝐴 ∈ ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) )
14 13 3 eleqtrrdi ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) → 𝐴𝑆 )
15 10 subgbas ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 = ( Base ‘ ( 𝐺s 𝑆 ) ) )
16 9 15 syl ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) → 𝑆 = ( Base ‘ ( 𝐺s 𝑆 ) ) )
17 14 16 eleqtrd ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) → 𝐴 ∈ ( Base ‘ ( 𝐺s 𝑆 ) ) )
18 16 eleq2d ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) → ( 𝑦𝑆𝑦 ∈ ( Base ‘ ( 𝐺s 𝑆 ) ) ) )
19 18 biimpar ( ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) ∧ 𝑦 ∈ ( Base ‘ ( 𝐺s 𝑆 ) ) ) → 𝑦𝑆 )
20 simpr ( ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) ∧ 𝑦𝑆 ) → 𝑦𝑆 )
21 20 3 eleqtrdi ( ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) ∧ 𝑦𝑆 ) → 𝑦 ∈ ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) )
22 oveq1 ( 𝑥 = 𝑛 → ( 𝑥 · 𝐴 ) = ( 𝑛 · 𝐴 ) )
23 22 cbvmptv ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐴 ) )
24 ovex ( 𝑛 · 𝐴 ) ∈ V
25 23 24 elrnmpti ( 𝑦 ∈ ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) ) ↔ ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝐴 ) )
26 21 25 sylib ( ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) ∧ 𝑦𝑆 ) → ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝐴 ) )
27 9 ad2antrr ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) ∧ 𝑦𝑆 ) ∧ 𝑛 ∈ ℤ ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
28 simpr ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) ∧ 𝑦𝑆 ) ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℤ )
29 14 ad2antrr ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) ∧ 𝑦𝑆 ) ∧ 𝑛 ∈ ℤ ) → 𝐴𝑆 )
30 2 10 5 subgmulg ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑛 ∈ ℤ ∧ 𝐴𝑆 ) → ( 𝑛 · 𝐴 ) = ( 𝑛 ( .g ‘ ( 𝐺s 𝑆 ) ) 𝐴 ) )
31 27 28 29 30 syl3anc ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) ∧ 𝑦𝑆 ) ∧ 𝑛 ∈ ℤ ) → ( 𝑛 · 𝐴 ) = ( 𝑛 ( .g ‘ ( 𝐺s 𝑆 ) ) 𝐴 ) )
32 31 eqeq2d ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) ∧ 𝑦𝑆 ) ∧ 𝑛 ∈ ℤ ) → ( 𝑦 = ( 𝑛 · 𝐴 ) ↔ 𝑦 = ( 𝑛 ( .g ‘ ( 𝐺s 𝑆 ) ) 𝐴 ) ) )
33 32 rexbidva ( ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) ∧ 𝑦𝑆 ) → ( ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝐴 ) ↔ ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ ( 𝐺s 𝑆 ) ) 𝐴 ) ) )
34 26 33 mpbid ( ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) ∧ 𝑦𝑆 ) → ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ ( 𝐺s 𝑆 ) ) 𝐴 ) )
35 19 34 syldan ( ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) ∧ 𝑦 ∈ ( Base ‘ ( 𝐺s 𝑆 ) ) ) → ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 ( .g ‘ ( 𝐺s 𝑆 ) ) 𝐴 ) )
36 4 5 12 17 35 iscygd ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋 ) → ( 𝐺s 𝑆 ) ∈ CycGrp )