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 ⊢ · ˙ = ⋅ G
cycsubg2cl.k ⊢ K = mrCls ⁡ SubGrp ⁡ G
Assertion cycsubg2cl ⊢ G ∈ Grp ∧ A ∈ X ∧ N ∈ ℤ → N · ˙ A ∈ K ⁡ A

Proof

Step Hyp Ref Expression
1 cycsubg2cl.x ⊢ X = Base G
2 cycsubg2cl.t ⊢ · ˙ = ⋅ G
3 cycsubg2cl.k ⊢ K = mrCls ⁡ SubGrp ⁡ G
4 1 subgacs ⊢ G ∈ Grp → SubGrp ⁡ G ∈ ACS ⁡ X
5 4 acsmred ⊢ G ∈ Grp → SubGrp ⁡ G ∈ Moore ⁡ X
6 5 3ad2ant1 ⊢ G ∈ Grp ∧ A ∈ X ∧ N ∈ ℤ → SubGrp ⁡ G ∈ Moore ⁡ X
7 simp2 ⊢ G ∈ Grp ∧ A ∈ X ∧ N ∈ ℤ → A ∈ X
8 7 snssd ⊢ G ∈ Grp ∧ A ∈ X ∧ N ∈ ℤ → A ⊆ X
9 3 mrccl ⊢ SubGrp ⁡ G ∈ Moore ⁡ X ∧ A ⊆ X → K ⁡ A ∈ SubGrp ⁡ G
10 6 8 9 syl2anc ⊢ G ∈ Grp ∧ A ∈ X ∧ N ∈ ℤ → K ⁡ A ∈ SubGrp ⁡ G
11 simp3 ⊢ G ∈ Grp ∧ A ∈ X ∧ N ∈ ℤ → N ∈ ℤ
12 6 3 8 mrcssidd ⊢ G ∈ Grp ∧ A ∈ X ∧ N ∈ ℤ → A ⊆ K ⁡ A
13 snssg ⊢ A ∈ X → A ∈ K ⁡ A ↔ A ⊆ K ⁡ A
14 13 3ad2ant2 ⊢ G ∈ Grp ∧ A ∈ X ∧ N ∈ ℤ → A ∈ K ⁡ A ↔ A ⊆ K ⁡ A
15 12 14 mpbird ⊢ G ∈ Grp ∧ A ∈ X ∧ N ∈ ℤ → A ∈ K ⁡ A
16 2 subgmulgcl ⊢ K ⁡ A ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ A ∈ K ⁡ A → N · ˙ A ∈ K ⁡ A
17 10 11 15 16 syl3anc ⊢ G ∈ Grp ∧ A ∈ X ∧ N ∈ ℤ → N · ˙ A ∈ K ⁡ A