Metamath Proof Explorer


Theorem cycsubg2

Description: The subgroup generated by an element is exhausted by its multiples. (Contributed by Stefan O'Rear, 6-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 cycsubg2.x
 |-  X = ( Base ` G )
2 cycsubg2.t
 |-  .x. = ( .g ` G )
3 cycsubg2.f
 |-  F = ( x e. ZZ |-> ( x .x. A ) )
4 cycsubg2.k
 |-  K = ( mrCls ` ( SubGrp ` G ) )
5 snssg
 |-  ( A e. X -> ( A e. y <-> { A } C_ y ) )
6 5 bicomd
 |-  ( A e. X -> ( { A } C_ y <-> A e. y ) )
7 6 adantl
 |-  ( ( G e. Grp /\ A e. X ) -> ( { A } C_ y <-> A e. y ) )
8 7 rabbidv
 |-  ( ( G e. Grp /\ A e. X ) -> { y e. ( SubGrp ` G ) | { A } C_ y } = { y e. ( SubGrp ` G ) | A e. y } )
9 8 inteqd
 |-  ( ( G e. Grp /\ A e. X ) -> |^| { y e. ( SubGrp ` G ) | { A } C_ y } = |^| { y e. ( SubGrp ` G ) | A e. y } )
10 1 subgacs
 |-  ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` X ) )
11 10 acsmred
 |-  ( G e. Grp -> ( SubGrp ` G ) e. ( Moore ` X ) )
12 snssi
 |-  ( A e. X -> { A } C_ X )
13 4 mrcval
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` X ) /\ { A } C_ X ) -> ( K ` { A } ) = |^| { y e. ( SubGrp ` G ) | { A } C_ y } )
14 11 12 13 syl2an
 |-  ( ( G e. Grp /\ A e. X ) -> ( K ` { A } ) = |^| { y e. ( SubGrp ` G ) | { A } C_ y } )
15 1 2 3 cycsubg
 |-  ( ( G e. Grp /\ A e. X ) -> ran F = |^| { y e. ( SubGrp ` G ) | A e. y } )
16 9 14 15 3eqtr4d
 |-  ( ( G e. Grp /\ A e. X ) -> ( K ` { A } ) = ran F )