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 )