Theorem cycsubggend

Description: The cyclic subgroup generated by A includes its generator. Although this theorem holds for any class G , the definition of F is only meaningful if G is a group. (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	cycsubggend.1	$$⊢B={\mathrm{Base}}_G$$
	cycsubggend.2	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	cycsubggend.3	$$⊢F=\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}A\right)$$
	cycsubggend.4	$$⊢\phi \to A\in B$$
Assertion	cycsubggend	$$⊢\phi \to A\in \mathrm{ran}F$$

Proof

Step	Hyp	Ref	Expression
1		cycsubggend.1	$$⊢B={\mathrm{Base}}_G$$
2		cycsubggend.2	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		cycsubggend.3	$$⊢F=\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}A\right)$$
4		cycsubggend.4	$$⊢\phi \to A\in B$$
5		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
6		simpr	$$⊢\left(\phi \wedge n=1\right)\to n=1$$
7	6	oveq1d	$$⊢\left(\phi \wedge n=1\right)\to n\underset{\dot{}}{·}A=1\underset{\dot{}}{·}A$$
8	4	adantr	$$⊢\left(\phi \wedge n=1\right)\to A\in B$$
9	1 2	mulg1	$$⊢A\in B\to 1\underset{\dot{}}{·}A=A$$
10	8 9	syl	$$⊢\left(\phi \wedge n=1\right)\to 1\underset{\dot{}}{·}A=A$$
11	7 10	eqtr2d	$$⊢\left(\phi \wedge n=1\right)\to A=n\underset{\dot{}}{·}A$$
12	3 5 4 11	elrnmptdv	$$⊢\phi \to A\in \mathrm{ran}F$$