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

Metamath Proof Explorer

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