Theorem fincygsubgd

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

	Ref	Expression
Hypotheses	fincygsubgd.1	$$⊢B={\mathrm{Base}}_G$$
	fincygsubgd.2	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	fincygsubgd.3	$$⊢H=\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}\left(C\underset{\dot{}}{·}A\right)\right)$$
	fincygsubgd.4	$$⊢\phi \to G\in \mathrm{Grp}$$
	fincygsubgd.5	$$⊢\phi \to A\in B$$
	fincygsubgd.6	$$⊢\phi \to C\in \mathbb{N}$$
Assertion	fincygsubgd	$$⊢\phi \to \mathrm{ran}H\in \mathrm{SubGrp}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		fincygsubgd.1	$$⊢B={\mathrm{Base}}_G$$
2		fincygsubgd.2	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		fincygsubgd.3	$$⊢H=\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}\left(C\underset{\dot{}}{·}A\right)\right)$$
4		fincygsubgd.4	$$⊢\phi \to G\in \mathrm{Grp}$$
5		fincygsubgd.5	$$⊢\phi \to A\in B$$
6		fincygsubgd.6	$$⊢\phi \to C\in \mathbb{N}$$
7	6	nnzd	$$⊢\phi \to C\in \mathbb{Z}$$
8	1 2 4 7 5	mulgcld	$$⊢\phi \to C\underset{\dot{}}{·}A\in B$$
9	1 2 3 4 8	cycsubgcld	$$⊢\phi \to \mathrm{ran}H\in \mathrm{SubGrp}\left(G\right)$$