Metamath Proof Explorer

Theorem cycsubmcmn

Description: The set of nonnegative integer powers of an element A of a monoid forms a commutative monoid. (Contributed by AV, 20-Jan-2024)

Ref Expression
Hypotheses cycsubmcmn.b ⊢ B = Base G
cycsubmcmn.t ⊢ · ˙ = ⋅ G
cycsubmcmn.f ⊢ F = x ∈ ℕ 0 ⟼ x · ˙ A
cycsubmcmn.c ⊢ C = ran ⁡ F
Assertion cycsubmcmn ⊢ G ∈ Mnd ∧ A ∈ B → G ↾ 𝑠 C ∈ CMnd

Proof

Step Hyp Ref Expression
1 cycsubmcmn.b ⊢ B = Base G
2 cycsubmcmn.t ⊢ · ˙ = ⋅ G
3 cycsubmcmn.f ⊢ F = x ∈ ℕ 0 ⟼ x · ˙ A
4 cycsubmcmn.c ⊢ C = ran ⁡ F
5 1 2 3 4 cycsubm ⊢ G ∈ Mnd ∧ A ∈ B → C ∈ SubMnd ⁡ G
6 eqid ⊢ 0 G = 0 G
7 eqid ⊢ G ↾ 𝑠 C = G ↾ 𝑠 C
8 1 6 7 issubm2 ⊢ G ∈ Mnd → C ∈ SubMnd ⁡ G ↔ C ⊆ B ∧ 0 G ∈ C ∧ G ↾ 𝑠 C ∈ Mnd
9 8 adantr ⊢ G ∈ Mnd ∧ A ∈ B → C ∈ SubMnd ⁡ G ↔ C ⊆ B ∧ 0 G ∈ C ∧ G ↾ 𝑠 C ∈ Mnd
10 simp3 ⊢ C ⊆ B ∧ 0 G ∈ C ∧ G ↾ 𝑠 C ∈ Mnd → G ↾ 𝑠 C ∈ Mnd
11 9 10 biimtrdi ⊢ G ∈ Mnd ∧ A ∈ B → C ∈ SubMnd ⁡ G → G ↾ 𝑠 C ∈ Mnd
12 5 11 mpd ⊢ G ∈ Mnd ∧ A ∈ B → G ↾ 𝑠 C ∈ Mnd
13 7 submbas ⊢ C ∈ SubMnd ⁡ G → C = Base G ↾ 𝑠 C
14 5 13 syl ⊢ G ∈ Mnd ∧ A ∈ B → C = Base G ↾ 𝑠 C
15 14 eqcomd ⊢ G ∈ Mnd ∧ A ∈ B → Base G ↾ 𝑠 C = C
16 15 eleq2d ⊢ G ∈ Mnd ∧ A ∈ B → x ∈ Base G ↾ 𝑠 C ↔ x ∈ C
17 15 eleq2d ⊢ G ∈ Mnd ∧ A ∈ B → y ∈ Base G ↾ 𝑠 C ↔ y ∈ C
18 16 17 anbi12d ⊢ G ∈ Mnd ∧ A ∈ B → x ∈ Base G ↾ 𝑠 C ∧ y ∈ Base G ↾ 𝑠 C ↔ x ∈ C ∧ y ∈ C
19 eqid ⊢ + G = + G
20 1 2 3 4 19 cycsubmcom ⊢ G ∈ Mnd ∧ A ∈ B ∧ x ∈ C ∧ y ∈ C → x + G y = y + G x
21 5 adantr ⊢ G ∈ Mnd ∧ A ∈ B ∧ x ∈ C ∧ y ∈ C → C ∈ SubMnd ⁡ G
22 7 19 ressplusg ⊢ C ∈ SubMnd ⁡ G → + G = + G ↾ 𝑠 C
23 22 eqcomd ⊢ C ∈ SubMnd ⁡ G → + G ↾ 𝑠 C = + G
24 23 oveqd ⊢ C ∈ SubMnd ⁡ G → x + G ↾ 𝑠 C y = x + G y
25 23 oveqd ⊢ C ∈ SubMnd ⁡ G → y + G ↾ 𝑠 C x = y + G x
26 24 25 eqeq12d ⊢ C ∈ SubMnd ⁡ G → x + G ↾ 𝑠 C y = y + G ↾ 𝑠 C x ↔ x + G y = y + G x
27 21 26 syl ⊢ G ∈ Mnd ∧ A ∈ B ∧ x ∈ C ∧ y ∈ C → x + G ↾ 𝑠 C y = y + G ↾ 𝑠 C x ↔ x + G y = y + G x
28 20 27 mpbird ⊢ G ∈ Mnd ∧ A ∈ B ∧ x ∈ C ∧ y ∈ C → x + G ↾ 𝑠 C y = y + G ↾ 𝑠 C x
29 28 ex ⊢ G ∈ Mnd ∧ A ∈ B → x ∈ C ∧ y ∈ C → x + G ↾ 𝑠 C y = y + G ↾ 𝑠 C x
30 18 29 sylbid ⊢ G ∈ Mnd ∧ A ∈ B → x ∈ Base G ↾ 𝑠 C ∧ y ∈ Base G ↾ 𝑠 C → x + G ↾ 𝑠 C y = y + G ↾ 𝑠 C x
31 30 ralrimivv ⊢ G ∈ Mnd ∧ A ∈ B → ∀ x ∈ Base G ↾ 𝑠 C ∀ y ∈ Base G ↾ 𝑠 C x + G ↾ 𝑠 C y = y + G ↾ 𝑠 C x
32 eqid ⊢ Base G ↾ 𝑠 C = Base G ↾ 𝑠 C
33 eqid ⊢ + G ↾ 𝑠 C = + G ↾ 𝑠 C
34 32 33 iscmn ⊢ G ↾ 𝑠 C ∈ CMnd ↔ G ↾ 𝑠 C ∈ Mnd ∧ ∀ x ∈ Base G ↾ 𝑠 C ∀ y ∈ Base G ↾ 𝑠 C x + G ↾ 𝑠 C y = y + G ↾ 𝑠 C x
35 12 31 34 sylanbrc ⊢ G ∈ Mnd ∧ A ∈ B → G ↾ 𝑠 C ∈ CMnd