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 )