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 ⊢ B = Base G
cycsubm.t ⊢ · ˙ = ⋅ G
cycsubm.f ⊢ F = x ∈ ℕ 0 ⟼ x · ˙ A
cycsubm.c ⊢ C = ran ⁡ F
Assertion cycsubmcl ⊢ A ∈ B → A ∈ C

Proof

Step Hyp Ref Expression
1 cycsubm.b ⊢ B = Base G
2 cycsubm.t ⊢ · ˙ = ⋅ G
3 cycsubm.f ⊢ F = x ∈ ℕ 0 ⟼ x · ˙ A
4 cycsubm.c ⊢ C = ran ⁡ F
5 1nn0 ⊢ 1 ∈ ℕ 0
6 5 a1i ⊢ A ∈ B → 1 ∈ ℕ 0
7 oveq1 ⊢ i = 1 → i · ˙ A = 1 · ˙ A
8 7 eqeq2d ⊢ i = 1 → A = i · ˙ A ↔ A = 1 · ˙ A
9 8 adantl ⊢ A ∈ B ∧ i = 1 → A = i · ˙ A ↔ A = 1 · ˙ A
10 1 2 mulg1 ⊢ A ∈ B → 1 · ˙ A = A
11 10 eqcomd ⊢ A ∈ B → A = 1 · ˙ A
12 6 9 11 rspcedvd ⊢ A ∈ B → ∃ i ∈ ℕ 0 A = i · ˙ A
13 1 2 3 4 cycsubmel ⊢ A ∈ C ↔ ∃ i ∈ ℕ 0 A = i · ˙ A
14 12 13 sylibr ⊢ A ∈ B → A ∈ C