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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	cycsubgcld.2	⊢ · = ( .g ‘ 𝐺 )
	cycsubgcld.3	⊢ 𝐹 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐴 ) )
	cycsubgcld.4	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	cycsubgcld.5	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
Assertion	cycsubgcld	⊢ ( 𝜑 → ran 𝐹 ∈ ( SubGrp ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		cycsubgcld.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		cycsubgcld.2	⊢ · = ( .g ‘ 𝐺 )
3		cycsubgcld.3	⊢ 𝐹 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐴 ) )
4		cycsubgcld.4	⊢ ( 𝜑 → 𝐺 ∈ Grp )
5		cycsubgcld.5	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
6	1 2 3	cycsubgcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵 ) → ( ran 𝐹 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ran 𝐹 ) )
7	4 5 6	syl2anc	⊢ ( 𝜑 → ( ran 𝐹 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ran 𝐹 ) )
8	7	simpld	⊢ ( 𝜑 → ran 𝐹 ∈ ( SubGrp ‘ 𝐺 ) )