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 
|- 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 )