Metamath Proof Explorer


Theorem cycsubg

Description: The cyclic group generated by A is the smallest subgroup containing A . (Contributed by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypotheses cycsubg.x
|- X = ( Base ` G )
cycsubg.t
|- .x. = ( .g ` G )
cycsubg.f
|- F = ( x e. ZZ |-> ( x .x. A ) )
Assertion cycsubg
|- ( ( G e. Grp /\ A e. X ) -> ran F = |^| { s e. ( SubGrp ` G ) | A e. s } )

Proof

Step Hyp Ref Expression
1 cycsubg.x
 |-  X = ( Base ` G )
2 cycsubg.t
 |-  .x. = ( .g ` G )
3 cycsubg.f
 |-  F = ( x e. ZZ |-> ( x .x. A ) )
4 ssintab
 |-  ( ran F C_ |^| { s | ( s e. ( SubGrp ` G ) /\ A e. s ) } <-> A. s ( ( s e. ( SubGrp ` G ) /\ A e. s ) -> ran F C_ s ) )
5 1 2 3 cycsubgss
 |-  ( ( s e. ( SubGrp ` G ) /\ A e. s ) -> ran F C_ s )
6 4 5 mpgbir
 |-  ran F C_ |^| { s | ( s e. ( SubGrp ` G ) /\ A e. s ) }
7 df-rab
 |-  { s e. ( SubGrp ` G ) | A e. s } = { s | ( s e. ( SubGrp ` G ) /\ A e. s ) }
8 7 inteqi
 |-  |^| { s e. ( SubGrp ` G ) | A e. s } = |^| { s | ( s e. ( SubGrp ` G ) /\ A e. s ) }
9 6 8 sseqtrri
 |-  ran F C_ |^| { s e. ( SubGrp ` G ) | A e. s }
10 9 a1i
 |-  ( ( G e. Grp /\ A e. X ) -> ran F C_ |^| { s e. ( SubGrp ` G ) | A e. s } )
11 1 2 3 cycsubgcl
 |-  ( ( G e. Grp /\ A e. X ) -> ( ran F e. ( SubGrp ` G ) /\ A e. ran F ) )
12 eleq2
 |-  ( s = ran F -> ( A e. s <-> A e. ran F ) )
13 12 elrab
 |-  ( ran F e. { s e. ( SubGrp ` G ) | A e. s } <-> ( ran F e. ( SubGrp ` G ) /\ A e. ran F ) )
14 11 13 sylibr
 |-  ( ( G e. Grp /\ A e. X ) -> ran F e. { s e. ( SubGrp ` G ) | A e. s } )
15 intss1
 |-  ( ran F e. { s e. ( SubGrp ` G ) | A e. s } -> |^| { s e. ( SubGrp ` G ) | A e. s } C_ ran F )
16 14 15 syl
 |-  ( ( G e. Grp /\ A e. X ) -> |^| { s e. ( SubGrp ` G ) | A e. s } C_ ran F )
17 10 16 eqssd
 |-  ( ( G e. Grp /\ A e. X ) -> ran F = |^| { s e. ( SubGrp ` G ) | A e. s } )