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 )