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 e. Grp /\ A e. B ) -> ( G |`s ( K ` { A } ) ) e. CycGrp )

Proof

Step	Hyp	Ref	Expression
1		cycsubgcyg2.b	|- B = ( Base ` G )
2		cycsubgcyg2.k	|- K = ( mrCls ` ( SubGrp ` G ) )
3		eqid	|- ( .g ` G ) = ( .g ` G )
4		eqid	|- ( n e. ZZ |-> ( n ( .g ` G ) A ) ) = ( n e. ZZ |-> ( n ( .g ` G ) A ) )
5	1 3 4 2	cycsubg2	|- ( ( G e. Grp /\ A e. B ) -> ( K ` { A } ) = ran ( n e. ZZ |-> ( n ( .g ` G ) A ) ) )
6	5	oveq2d	|- ( ( G e. Grp /\ A e. B ) -> ( G |`s ( K ` { A } ) ) = ( G |`s ran ( n e. ZZ |-> ( n ( .g ` G ) A ) ) ) )
7		eqid	|- ran ( n e. ZZ |-> ( n ( .g ` G ) A ) ) = ran ( n e. ZZ |-> ( n ( .g ` G ) A ) )
8	1 3 7	cycsubgcyg	|- ( ( G e. Grp /\ A e. B ) -> ( G |`s ran ( n e. ZZ |-> ( n ( .g ` G ) A ) ) ) e. CycGrp )
9	6 8	eqeltrd	|- ( ( G e. Grp /\ A e. B ) -> ( G |`s ( K ` { A } ) ) e. CycGrp )