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=BaseG
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=BaseG
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 ⊢0G=0G
7 eqid ⊢G↾𝑠C=G↾𝑠C
8 1 6 7 issubm2 ⊢G∈Mnd→C∈SubMnd⁡G↔C⊆B∧0G∈C∧G↾𝑠C∈Mnd
9 8 adantr ⊢G∈Mnd∧A∈B→C∈SubMnd⁡G↔C⊆B∧0G∈C∧G↾𝑠C∈Mnd
10 simp3 ⊢C⊆B∧0G∈C∧G↾𝑠C∈Mnd→G↾𝑠C∈Mnd
11 9 10 syl6bi ⊢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=BaseG↾𝑠C
14 5 13 syl ⊢G∈Mnd∧A∈B→C=BaseG↾𝑠C
15 14 eqcomd ⊢G∈Mnd∧A∈B→BaseG↾𝑠C=C
16 15 eleq2d ⊢G∈Mnd∧A∈B→x∈BaseG↾𝑠C↔x∈C
17 15 eleq2d ⊢G∈Mnd∧A∈B→y∈BaseG↾𝑠C↔y∈C
18 16 17 anbi12d ⊢G∈Mnd∧A∈B→x∈BaseG↾𝑠C∧y∈BaseG↾𝑠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+Gy=y+Gx
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↾𝑠Cy=x+Gy
25 23 oveqd ⊢C∈SubMnd⁡G→y+G↾𝑠Cx=y+Gx
26 24 25 eqeq12d ⊢C∈SubMnd⁡G→x+G↾𝑠Cy=y+G↾𝑠Cx↔x+Gy=y+Gx
27 21 26 syl ⊢G∈Mnd∧A∈B∧x∈C∧y∈C→x+G↾𝑠Cy=y+G↾𝑠Cx↔x+Gy=y+Gx
28 20 27 mpbird ⊢G∈Mnd∧A∈B∧x∈C∧y∈C→x+G↾𝑠Cy=y+G↾𝑠Cx
29 28 ex ⊢G∈Mnd∧A∈B→x∈C∧y∈C→x+G↾𝑠Cy=y+G↾𝑠Cx
30 18 29 sylbid ⊢G∈Mnd∧A∈B→x∈BaseG↾𝑠C∧y∈BaseG↾𝑠C→x+G↾𝑠Cy=y+G↾𝑠Cx
31 30 ralrimivv ⊢G∈Mnd∧A∈B→∀x∈BaseG↾𝑠C∀y∈BaseG↾𝑠Cx+G↾𝑠Cy=y+G↾𝑠Cx
32 eqid ⊢BaseG↾𝑠C=BaseG↾𝑠C
33 eqid ⊢+G↾𝑠C=+G↾𝑠C
34 32 33 iscmn ⊢G↾𝑠C∈CMnd↔G↾𝑠C∈Mnd∧∀x∈BaseG↾𝑠C∀y∈BaseG↾𝑠Cx+G↾𝑠Cy=y+G↾𝑠Cx
35 12 31 34 sylanbrc ⊢G∈Mnd∧A∈B→G↾𝑠C∈CMnd