This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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