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 𝐵 = ( Base ‘ 𝐺 )
cycsubgcyg2.k 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
Assertion cycsubgcyg2 ( ( 𝐺 ∈ Grp ∧ 𝐴𝐵 ) → ( 𝐺s ( 𝐾 ‘ { 𝐴 } ) ) ∈ CycGrp )

Proof

Step Hyp Ref Expression
1 cycsubgcyg2.b 𝐵 = ( Base ‘ 𝐺 )
2 cycsubgcyg2.k 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
3 eqid ( .g𝐺 ) = ( .g𝐺 )
4 eqid ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g𝐺 ) 𝐴 ) ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g𝐺 ) 𝐴 ) )
5 1 3 4 2 cycsubg2 ( ( 𝐺 ∈ Grp ∧ 𝐴𝐵 ) → ( 𝐾 ‘ { 𝐴 } ) = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g𝐺 ) 𝐴 ) ) )
6 5 oveq2d ( ( 𝐺 ∈ Grp ∧ 𝐴𝐵 ) → ( 𝐺s ( 𝐾 ‘ { 𝐴 } ) ) = ( 𝐺s ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g𝐺 ) 𝐴 ) ) ) )
7 eqid ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g𝐺 ) 𝐴 ) ) = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g𝐺 ) 𝐴 ) )
8 1 3 7 cycsubgcyg ( ( 𝐺 ∈ Grp ∧ 𝐴𝐵 ) → ( 𝐺s ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g𝐺 ) 𝐴 ) ) ) ∈ CycGrp )
9 6 8 eqeltrd ( ( 𝐺 ∈ Grp ∧ 𝐴𝐵 ) → ( 𝐺s ( 𝐾 ‘ { 𝐴 } ) ) ∈ CycGrp )