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

Metamath Proof Explorer

Theorem cycsubgcld

Description: The cyclic subgroup generated by A is a subgroup. Deduction related to cycsubgcl . (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses cycsubgcld.1 ⊢ B = Base G
cycsubgcld.2 ⊢ · ˙ = ⋅ G
cycsubgcld.3 ⊢ F = n ∈ ℤ ⟼ n · ˙ A
cycsubgcld.4 ⊢ φ → G ∈ Grp
cycsubgcld.5 ⊢ φ → A ∈ B
Assertion cycsubgcld ⊢ φ → ran ⁡ F ∈ SubGrp ⁡ G

Proof

Step Hyp Ref Expression
1 cycsubgcld.1 ⊢ B = Base G
2 cycsubgcld.2 ⊢ · ˙ = ⋅ G
3 cycsubgcld.3 ⊢ F = n ∈ ℤ ⟼ n · ˙ A
4 cycsubgcld.4 ⊢ φ → G ∈ Grp
5 cycsubgcld.5 ⊢ φ → A ∈ B
6 1 2 3 cycsubgcl ⊢ G ∈ Grp ∧ A ∈ B → ran ⁡ F ∈ SubGrp ⁡ G ∧ A ∈ ran ⁡ F
7 4 5 6 syl2anc ⊢ φ → ran ⁡ F ∈ SubGrp ⁡ G ∧ A ∈ ran ⁡ F
8 7 simpld ⊢ φ → ran ⁡ F ∈ SubGrp ⁡ G