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	|- .x. = ( .g ` G )
	cycsubgcld.3	|- F = ( n e. ZZ |-> ( n .x. A ) )
	cycsubgcld.4	|- ( ph -> G e. Grp )
	cycsubgcld.5	|- ( ph -> A e. B )
Assertion	cycsubgcld	|- ( ph -> ran F e. ( SubGrp ` G ) )

Proof

Step	Hyp	Ref	Expression
1		cycsubgcld.1	|- B = ( Base ` G )
2		cycsubgcld.2	|- .x. = ( .g ` G )
3		cycsubgcld.3	|- F = ( n e. ZZ |-> ( n .x. A ) )
4		cycsubgcld.4	|- ( ph -> G e. Grp )
5		cycsubgcld.5	|- ( ph -> A e. B )
6	1 2 3	cycsubgcl	|- ( ( G e. Grp /\ A e. B ) -> ( ran F e. ( SubGrp ` G ) /\ A e. ran F ) )
7	4 5 6	syl2anc	|- ( ph -> ( ran F e. ( SubGrp ` G ) /\ A e. ran F ) )
8	7	simpld	|- ( ph -> ran F e. ( SubGrp ` G ) )