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={\mathrm{Base}}_G$$
	cycsubgcld.2	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	cycsubgcld.3	$$⊢F=\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}A\right)$$
	cycsubgcld.4	$$⊢\phi \to G\in \mathrm{Grp}$$
	cycsubgcld.5	$$⊢\phi \to A\in B$$
Assertion	cycsubgcld	$$⊢\phi \to \mathrm{ran}F\in \mathrm{SubGrp}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		cycsubgcld.1	$$⊢B={\mathrm{Base}}_G$$
2		cycsubgcld.2	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		cycsubgcld.3	$$⊢F=\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}A\right)$$
4		cycsubgcld.4	$$⊢\phi \to G\in \mathrm{Grp}$$
5		cycsubgcld.5	$$⊢\phi \to A\in B$$
6	1 2 3	cycsubgcl	$$⊢\left(G\in \mathrm{Grp}\wedge A\in B\right)\to \left(\mathrm{ran}F\in \mathrm{SubGrp}\left(G\right)\wedge A\in \mathrm{ran}F\right)$$
7	4 5 6	syl2anc	$$⊢\phi \to \left(\mathrm{ran}F\in \mathrm{SubGrp}\left(G\right)\wedge A\in \mathrm{ran}F\right)$$
8	7	simpld	$$⊢\phi \to \mathrm{ran}F\in \mathrm{SubGrp}\left(G\right)$$