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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	cycsubm.t	⊢ · = ( .g ‘ 𝐺 )
	cycsubm.f	⊢ 𝐹 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 · 𝐴 ) )
	cycsubm.c	⊢ 𝐶 = ran 𝐹
Assertion	cycsubmcl	⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		cycsubm.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		cycsubm.t	⊢ · = ( .g ‘ 𝐺 )
3		cycsubm.f	⊢ 𝐹 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 · 𝐴 ) )
4		cycsubm.c	⊢ 𝐶 = ran 𝐹
5		1nn0	⊢ 1 ∈ ℕ0
6	5	a1i	⊢ ( 𝐴 ∈ 𝐵 → 1 ∈ ℕ0 )
7		oveq1	⊢ ( 𝑖 = 1 → ( 𝑖 · 𝐴 ) = ( 1 · 𝐴 ) )
8	7	eqeq2d	⊢ ( 𝑖 = 1 → ( 𝐴 = ( 𝑖 · 𝐴 ) ↔ 𝐴 = ( 1 · 𝐴 ) ) )
9	8	adantl	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝑖 = 1 ) → ( 𝐴 = ( 𝑖 · 𝐴 ) ↔ 𝐴 = ( 1 · 𝐴 ) ) )
10	1 2	mulg1	⊢ ( 𝐴 ∈ 𝐵 → ( 1 · 𝐴 ) = 𝐴 )
11	10	eqcomd	⊢ ( 𝐴 ∈ 𝐵 → 𝐴 = ( 1 · 𝐴 ) )
12	6 9 11	rspcedvd	⊢ ( 𝐴 ∈ 𝐵 → ∃ 𝑖 ∈ ℕ0 𝐴 = ( 𝑖 · 𝐴 ) )
13	1 2 3 4	cycsubmel	⊢ ( 𝐴 ∈ 𝐶 ↔ ∃ 𝑖 ∈ ℕ0 𝐴 = ( 𝑖 · 𝐴 ) )
14	12 13	sylibr	⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ∈ 𝐶 )