This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )