Theorem fincygsubgd

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

	Ref	Expression
Hypotheses	fincygsubgd.1	|- B = ( Base ` G )
	fincygsubgd.2	|- .x. = ( .g ` G )
	fincygsubgd.3	|- H = ( n e. ZZ |-> ( n .x. ( C .x. A ) ) )
	fincygsubgd.4	|- ( ph -> G e. Grp )
	fincygsubgd.5	|- ( ph -> A e. B )
	fincygsubgd.6	|- ( ph -> C e. NN )
Assertion	fincygsubgd	|- ( ph -> ran H e. ( SubGrp ` G ) )

Proof

Step	Hyp	Ref	Expression
1		fincygsubgd.1	|- B = ( Base ` G )
2		fincygsubgd.2	|- .x. = ( .g ` G )
3		fincygsubgd.3	|- H = ( n e. ZZ |-> ( n .x. ( C .x. A ) ) )
4		fincygsubgd.4	|- ( ph -> G e. Grp )
5		fincygsubgd.5	|- ( ph -> A e. B )
6		fincygsubgd.6	|- ( ph -> C e. NN )
7	6	nnzd	|- ( ph -> C e. ZZ )
8	1 2 4 7 5	mulgcld	|- ( ph -> ( C .x. A ) e. B )
9	1 2 3 4 8	cycsubgcld	|- ( ph -> ran H e. ( SubGrp ` G ) )