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	⊢ 𝑋 = ( Base ‘ 𝐺 )
	cycsubg2cl.t	⊢ · = ( .g ‘ 𝐺 )
	cycsubg2cl.k	⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
Assertion	cycsubg2cl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( 𝑁 · 𝐴 ) ∈ ( 𝐾 ‘ { 𝐴 } ) )

Proof

Step	Hyp	Ref	Expression
1		cycsubg2cl.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		cycsubg2cl.t	⊢ · = ( .g ‘ 𝐺 )
3		cycsubg2cl.k	⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
4	1	subgacs	⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝑋 ) )
5	4	acsmred	⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝑋 ) )
6	5	3ad2ant1	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝑋 ) )
7		simp2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → 𝐴 ∈ 𝑋 )
8	7	snssd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → { 𝐴 } ⊆ 𝑋 )
9	3	mrccl	⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝑋 ) ∧ { 𝐴 } ⊆ 𝑋 ) → ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) )
10	6 8 9	syl2anc	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) )
11		simp3	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
12	6 3 8	mrcssidd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → { 𝐴 } ⊆ ( 𝐾 ‘ { 𝐴 } ) )
13		snssg	⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 ∈ ( 𝐾 ‘ { 𝐴 } ) ↔ { 𝐴 } ⊆ ( 𝐾 ‘ { 𝐴 } ) ) )
14	13	3ad2ant2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ∈ ( 𝐾 ‘ { 𝐴 } ) ↔ { 𝐴 } ⊆ ( 𝐾 ‘ { 𝐴 } ) ) )
15	12 14	mpbird	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → 𝐴 ∈ ( 𝐾 ‘ { 𝐴 } ) )
16	2	subgmulgcl	⊢ ( ( ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ( 𝐾 ‘ { 𝐴 } ) ) → ( 𝑁 · 𝐴 ) ∈ ( 𝐾 ‘ { 𝐴 } ) )
17	10 11 15 16	syl3anc	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( 𝑁 · 𝐴 ) ∈ ( 𝐾 ‘ { 𝐴 } ) )