Metamath Proof Explorer

Theorem cycsubgcyg

Description: The cyclic subgroup generated by A is a cyclic group. (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses cycsubgcyg.x 
|- X = ( Base ` G )
cycsubgcyg.t 
|- .x. = ( .g ` G )
cycsubgcyg.s 
|- S = ran ( x e. ZZ |-> ( x .x. A ) )
Assertion cycsubgcyg 
|- ( ( G e. Grp /\ A e. X ) -> ( G |`s S ) e. CycGrp )

Proof

Step Hyp Ref Expression
1 cycsubgcyg.x 
 |-  X = ( Base ` G )
2 cycsubgcyg.t 
 |-  .x. = ( .g ` G )
3 cycsubgcyg.s 
 |-  S = ran ( x e. ZZ |-> ( x .x. A ) )
4 eqid 
 |-  ( Base ` ( G |`s S ) ) = ( Base ` ( G |`s S ) )
5 eqid 
 |-  ( .g ` ( G |`s S ) ) = ( .g ` ( G |`s S ) )
6 eqid 
 |-  ( x e. ZZ |-> ( x .x. A ) ) = ( x e. ZZ |-> ( x .x. A ) )
7 1 2 6 cycsubgcl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ran ( x e. ZZ |-> ( x .x. A ) ) e. ( SubGrp ` G ) /\ A e. ran ( x e. ZZ |-> ( x .x. A ) ) ) )
8 7 simpld 
 |-  ( ( G e. Grp /\ A e. X ) -> ran ( x e. ZZ |-> ( x .x. A ) ) e. ( SubGrp ` G ) )
9 3 8 eqeltrid 
 |-  ( ( G e. Grp /\ A e. X ) -> S e. ( SubGrp ` G ) )
10 eqid 
 |-  ( G |`s S ) = ( G |`s S )
11 10 subggrp 
 |-  ( S e. ( SubGrp ` G ) -> ( G |`s S ) e. Grp )
12 9 11 syl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( G |`s S ) e. Grp )
13 7 simprd 
 |-  ( ( G e. Grp /\ A e. X ) -> A e. ran ( x e. ZZ |-> ( x .x. A ) ) )
14 13 3 eleqtrrdi 
 |-  ( ( G e. Grp /\ A e. X ) -> A e. S )
15 10 subgbas 
 |-  ( S e. ( SubGrp ` G ) -> S = ( Base ` ( G |`s S ) ) )
16 9 15 syl 
 |-  ( ( G e. Grp /\ A e. X ) -> S = ( Base ` ( G |`s S ) ) )
17 14 16 eleqtrd 
 |-  ( ( G e. Grp /\ A e. X ) -> A e. ( Base ` ( G |`s S ) ) )
18 16 eleq2d 
 |-  ( ( G e. Grp /\ A e. X ) -> ( y e. S <-> y e. ( Base ` ( G |`s S ) ) ) )
19 18 biimpar 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ y e. ( Base ` ( G |`s S ) ) ) -> y e. S )
20 simpr 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ y e. S ) -> y e. S )
21 20 3 eleqtrdi 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ y e. S ) -> y e. ran ( x e. ZZ |-> ( x .x. A ) ) )
22 oveq1 
 |-  ( x = n -> ( x .x. A ) = ( n .x. A ) )
23 22 cbvmptv 
 |-  ( x e. ZZ |-> ( x .x. A ) ) = ( n e. ZZ |-> ( n .x. A ) )
24 ovex 
 |-  ( n .x. A ) e. _V
25 23 24 elrnmpti 
 |-  ( y e. ran ( x e. ZZ |-> ( x .x. A ) ) <-> E. n e. ZZ y = ( n .x. A ) )
26 21 25 sylib 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ y e. S ) -> E. n e. ZZ y = ( n .x. A ) )
27 9 ad2antrr 
 |-  ( ( ( ( G e. Grp /\ A e. X ) /\ y e. S ) /\ n e. ZZ ) -> S e. ( SubGrp ` G ) )
28 simpr 
 |-  ( ( ( ( G e. Grp /\ A e. X ) /\ y e. S ) /\ n e. ZZ ) -> n e. ZZ )
29 14 ad2antrr 
 |-  ( ( ( ( G e. Grp /\ A e. X ) /\ y e. S ) /\ n e. ZZ ) -> A e. S )
30 2 10 5 subgmulg 
 |-  ( ( S e. ( SubGrp ` G ) /\ n e. ZZ /\ A e. S ) -> ( n .x. A ) = ( n ( .g ` ( G |`s S ) ) A ) )
31 27 28 29 30 syl3anc 
 |-  ( ( ( ( G e. Grp /\ A e. X ) /\ y e. S ) /\ n e. ZZ ) -> ( n .x. A ) = ( n ( .g ` ( G |`s S ) ) A ) )
32 31 eqeq2d 
 |-  ( ( ( ( G e. Grp /\ A e. X ) /\ y e. S ) /\ n e. ZZ ) -> ( y = ( n .x. A ) <-> y = ( n ( .g ` ( G |`s S ) ) A ) ) )
33 32 rexbidva 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ y e. S ) -> ( E. n e. ZZ y = ( n .x. A ) <-> E. n e. ZZ y = ( n ( .g ` ( G |`s S ) ) A ) ) )
34 26 33 mpbid 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ y e. S ) -> E. n e. ZZ y = ( n ( .g ` ( G |`s S ) ) A ) )
35 19 34 syldan 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ y e. ( Base ` ( G |`s S ) ) ) -> E. n e. ZZ y = ( n ( .g ` ( G |`s S ) ) A ) )
36 4 5 12 17 35 iscygd 
 |-  ( ( G e. Grp /\ A e. X ) -> ( G |`s S ) e. CycGrp )