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 ⊢ 𝑋 = ( 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 ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( 𝑁 · 𝐴 ) ∈ ( 𝐾 ‘ { 𝐴 } ) )