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