Theorem fincygsubgd

Description: The subgroup referenced in fincygsubgodd is a subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	fincygsubgd.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
	fincygsubgd.2	⊢ · = ( .g ‘ 𝐺 )
	fincygsubgd.3	⊢ 𝐻 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝐶 · 𝐴 ) ) )
	fincygsubgd.4	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	fincygsubgd.5	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	fincygsubgd.6	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
Assertion	fincygsubgd	⊢ ( 𝜑 → ran 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		fincygsubgd.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		fincygsubgd.2	⊢ · = ( .g ‘ 𝐺 )
3		fincygsubgd.3	⊢ 𝐻 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝐶 · 𝐴 ) ) )
4		fincygsubgd.4	⊢ ( 𝜑 → 𝐺 ∈ Grp )
5		fincygsubgd.5	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
6		fincygsubgd.6	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
7	6	nnzd	⊢ ( 𝜑 → 𝐶 ∈ ℤ )
8	1 2 4 7 5	mulgcld	⊢ ( 𝜑 → ( 𝐶 · 𝐴 ) ∈ 𝐵 )
9	1 2 3 4 8	cycsubgcld	⊢ ( 𝜑 → ran 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )