Theorem cycsubg2cl

Description: Any multiple of an element is contained in the generated cyclic subgroup. (Contributed by Stefan O'Rear, 12-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		cycsubg2cl.x	|- X = ( Base ` G )
2		cycsubg2cl.t	|- .x. = ( .g ` G )
3		cycsubg2cl.k	|- K = ( mrCls ` ( SubGrp ` G ) )
4	1	subgacs	|- ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` X ) )
5	4	acsmred	|- ( G e. Grp -> ( SubGrp ` G ) e. ( Moore ` X ) )
6	5	3ad2ant1	|- ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( SubGrp ` G ) e. ( Moore ` X ) )
7		simp2	|- ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> A e. X )
8	7	snssd	|- ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> { A } C_ X )
9	3	mrccl	|- ( ( ( SubGrp ` G ) e. ( Moore ` X ) /\ { A } C_ X ) -> ( K ` { A } ) e. ( SubGrp ` G ) )
10	6 8 9	syl2anc	|- ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( K ` { A } ) e. ( SubGrp ` G ) )
11		simp3	|- ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> N e. ZZ )
12	6 3 8	mrcssidd	|- ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> { A } C_ ( K ` { A } ) )
13		snssg	|- ( A e. X -> ( A e. ( K ` { A } ) <-> { A } C_ ( K ` { A } ) ) )
14	13	3ad2ant2	|- ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( A e. ( K ` { A } ) <-> { A } C_ ( K ` { A } ) ) )
15	12 14	mpbird	|- ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> A e. ( K ` { A } ) )
16	2	subgmulgcl	|- ( ( ( K ` { A } ) e. ( SubGrp ` G ) /\ N e. ZZ /\ A e. ( K ` { A } ) ) -> ( N .x. A ) e. ( K ` { A } ) )
17	10 11 15 16	syl3anc	|- ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( N .x. A ) e. ( K ` { A } ) )