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 = Base G
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 = Base G
2 cycsubgcyg2.k ⊢ K = mrCls ⁡ SubGrp ⁡ G
3 eqid ⊢ ⋅ G = ⋅ G
4 eqid ⊢ n ∈ ℤ ⟼ n ⋅ G A = n ∈ ℤ ⟼ n ⋅ G A
5 1 3 4 2 cycsubg2 ⊢ G ∈ Grp ∧ A ∈ B → K ⁡ A = ran ⁡ n ∈ ℤ ⟼ n ⋅ G A
6 5 oveq2d ⊢ G ∈ Grp ∧ A ∈ B → G ↾ 𝑠 K ⁡ A = G ↾ 𝑠 ran ⁡ n ∈ ℤ ⟼ n ⋅ G A
7 eqid ⊢ ran ⁡ n ∈ ℤ ⟼ n ⋅ G A = ran ⁡ n ∈ ℤ ⟼ n ⋅ G A
8 1 3 7 cycsubgcyg ⊢ G ∈ Grp ∧ A ∈ B → G ↾ 𝑠 ran ⁡ n ∈ ℤ ⟼ n ⋅ G A ∈ CycGrp
9 6 8 eqeltrd ⊢ G ∈ Grp ∧ A ∈ B → G ↾ 𝑠 K ⁡ A ∈ CycGrp