Theorem cycsubmcl

Description: The set of nonnegative integer powers of an element A contains A . Although this theorem holds for any class G , the definition of F is only meaningful if G is a monoid or at least a unital magma. (Contributed by AV, 28-Dec-2023)

	Ref	Expression
Hypotheses	cycsubm.b	$$⊢B={\mathrm{Base}}_G$$
	cycsubm.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	cycsubm.f	$$⊢F=\left(x\in {\mathbb{N}}_0⟼x\underset{\dot{}}{·}A\right)$$
	cycsubm.c	$$⊢C=\mathrm{ran}F$$
Assertion	cycsubmcl	$$⊢A\in B\to A\in C$$

Proof

Step	Hyp	Ref	Expression
1		cycsubm.b	$$⊢B={\mathrm{Base}}_G$$
2		cycsubm.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		cycsubm.f	$$⊢F=\left(x\in {\mathbb{N}}_0⟼x\underset{\dot{}}{·}A\right)$$
4		cycsubm.c	$$⊢C=\mathrm{ran}F$$
5		1nn0	$$⊢1\in {\mathbb{N}}_0$$
6	5	a1i	$$⊢A\in B\to 1\in {\mathbb{N}}_0$$
7		oveq1	$$⊢i=1\to i\underset{\dot{}}{·}A=1\underset{\dot{}}{·}A$$
8	7	eqeq2d	$$⊢i=1\to \left(A=i\underset{\dot{}}{·}A\leftrightarrow A=1\underset{\dot{}}{·}A\right)$$
9	8	adantl	$$⊢\left(A\in B\wedge i=1\right)\to \left(A=i\underset{\dot{}}{·}A\leftrightarrow A=1\underset{\dot{}}{·}A\right)$$
10	1 2	mulg1	$$⊢A\in B\to 1\underset{\dot{}}{·}A=A$$
11	10	eqcomd	$$⊢A\in B\to A=1\underset{\dot{}}{·}A$$
12	6 9 11	rspcedvd	$$⊢A\in B\to \exists i\in {\mathbb{N}}_{0}A=i\underset{\dot{}}{·}A$$
13	1 2 3 4	cycsubmel	$$⊢A\in C\leftrightarrow \exists i\in {\mathbb{N}}_{0}A=i\underset{\dot{}}{·}A$$
14	12 13	sylibr	$$⊢A\in B\to A\in C$$