Metamath Proof Explorer

Theorem cycsubg2

Description: The subgroup generated by an element is exhausted by its multiples. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Hypotheses cycsubg2.x ⊢ X = Base G
cycsubg2.t ⊢ · ˙ = ⋅ G
cycsubg2.f ⊢ F = x ∈ ℤ ⟼ x · ˙ A
cycsubg2.k ⊢ K = mrCls ⁡ SubGrp ⁡ G
Assertion cycsubg2 ⊢ G ∈ Grp ∧ A ∈ X → K ⁡ A = ran ⁡ F

Proof

Step Hyp Ref Expression
1 cycsubg2.x ⊢ X = Base G
2 cycsubg2.t ⊢ · ˙ = ⋅ G
3 cycsubg2.f ⊢ F = x ∈ ℤ ⟼ x · ˙ A
4 cycsubg2.k ⊢ K = mrCls ⁡ SubGrp ⁡ G
5 snssg ⊢ A ∈ X → A ∈ y ↔ A ⊆ y
6 5 bicomd ⊢ A ∈ X → A ⊆ y ↔ A ∈ y
7 6 adantl ⊢ G ∈ Grp ∧ A ∈ X → A ⊆ y ↔ A ∈ y
8 7 rabbidv ⊢ G ∈ Grp ∧ A ∈ X → y ∈ SubGrp ⁡ G | A ⊆ y = y ∈ SubGrp ⁡ G | A ∈ y
9 8 inteqd ⊢ G ∈ Grp ∧ A ∈ X → ⋂ y ∈ SubGrp ⁡ G | A ⊆ y = ⋂ y ∈ SubGrp ⁡ G | A ∈ y
10 1 subgacs ⊢ G ∈ Grp → SubGrp ⁡ G ∈ ACS ⁡ X
11 10 acsmred ⊢ G ∈ Grp → SubGrp ⁡ G ∈ Moore ⁡ X
12 snssi ⊢ A ∈ X → A ⊆ X
13 4 mrcval ⊢ SubGrp ⁡ G ∈ Moore ⁡ X ∧ A ⊆ X → K ⁡ A = ⋂ y ∈ SubGrp ⁡ G | A ⊆ y
14 11 12 13 syl2an ⊢ G ∈ Grp ∧ A ∈ X → K ⁡ A = ⋂ y ∈ SubGrp ⁡ G | A ⊆ y
15 1 2 3 cycsubg ⊢ G ∈ Grp ∧ A ∈ X → ran ⁡ F = ⋂ y ∈ SubGrp ⁡ G | A ∈ y
16 9 14 15 3eqtr4d ⊢ G ∈ Grp ∧ A ∈ X → K ⁡ A = ran ⁡ F