Theorem iscyggen

Description: The property of being a cyclic generator for a group. (Contributed by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	iscyg.1	$$⊢B={\mathrm{Base}}_G$$
	iscyg.2	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	iscyg3.e	$$⊢E=\left\{x\in B|\mathrm{ran}\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}x\right)=B\right\}$$
Assertion	iscyggen	$$⊢X\in E\leftrightarrow \left(X\in B\wedge \mathrm{ran}\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}X\right)=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		iscyg.1	$$⊢B={\mathrm{Base}}_G$$
2		iscyg.2	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		iscyg3.e	$$⊢E=\left\{x\in B|\mathrm{ran}\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}x\right)=B\right\}$$
4		simpl	$$⊢\left(x=X\wedge n\in \mathbb{Z}\right)\to x=X$$
5	4	oveq2d	$$⊢\left(x=X\wedge n\in \mathbb{Z}\right)\to n\underset{\dot{}}{·}x=n\underset{\dot{}}{·}X$$
6	5	mpteq2dva	$$⊢x=X\to \left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}x\right)=\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}X\right)$$
7	6	rneqd	$$⊢x=X\to \mathrm{ran}\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}x\right)=\mathrm{ran}\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}X\right)$$
8	7	eqeq1d	$$⊢x=X\to \left(\mathrm{ran}\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}x\right)=B\leftrightarrow \mathrm{ran}\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}X\right)=B\right)$$
9	8 3	elrab2	$$⊢X\in E\leftrightarrow \left(X\in B\wedge \mathrm{ran}\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}X\right)=B\right)$$