Metamath Proof Explorer

Theorem cycsubgcyg2

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

Ref Expression
Hypotheses cycsubgcyg2.b ⊢B=BaseG
cycsubgcyg2.k ⊢K=mrCls⁡SubGrp⁡G
Assertion cycsubgcyg2 ⊢G∈Grp∧A∈B→G↾𝑠K⁡A∈CycGrp

Proof

Step Hyp Ref Expression
1 cycsubgcyg2.b ⊢B=BaseG
2 cycsubgcyg2.k ⊢K=mrCls⁡SubGrp⁡G
3 eqid ⊢⋅G=⋅G
4 eqid ⊢n∈ℤ⟼n⋅GA=n∈ℤ⟼n⋅GA
5 1 3 4 2 cycsubg2 ⊢G∈Grp∧A∈B→K⁡A=ran⁡n∈ℤ⟼n⋅GA
6 5 oveq2d ⊢G∈Grp∧A∈B→G↾𝑠K⁡A=G↾𝑠ran⁡n∈ℤ⟼n⋅GA
7 eqid ⊢ran⁡n∈ℤ⟼n⋅GA=ran⁡n∈ℤ⟼n⋅GA
8 1 3 7 cycsubgcyg ⊢G∈Grp∧A∈B→G↾𝑠ran⁡n∈ℤ⟼n⋅GA∈CycGrp
9 6 8 eqeltrd ⊢G∈Grp∧A∈B→G↾𝑠K⁡A∈CycGrp