This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ∈ 𝐶 )