Metamath Proof Explorer


Theorem cycsubmcom

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

Ref Expression
Hypotheses cycsubmcom.b B = Base G
cycsubmcom.t · ˙ = G
cycsubmcom.f F = x 0 x · ˙ A
cycsubmcom.c C = ran F
cycsubmcom.p + ˙ = + G
Assertion cycsubmcom G Mnd A B X C Y C X + ˙ Y = Y + ˙ X

Proof

Step Hyp Ref Expression
1 cycsubmcom.b B = Base G
2 cycsubmcom.t · ˙ = G
3 cycsubmcom.f F = x 0 x · ˙ A
4 cycsubmcom.c C = ran F
5 cycsubmcom.p + ˙ = + G
6 1 2 3 4 cycsubmel c C i 0 c = i · ˙ A
7 6 biimpi c C i 0 c = i · ˙ A
8 7 adantl G Mnd A B X C Y C c C i 0 c = i · ˙ A
9 8 ralrimiva G Mnd A B X C Y C c C i 0 c = i · ˙ A
10 simplll G Mnd A B X C Y C m 0 n 0 G Mnd
11 simprl G Mnd A B X C Y C m 0 n 0 m 0
12 simprr G Mnd A B X C Y C m 0 n 0 n 0
13 simpllr G Mnd A B X C Y C m 0 n 0 A B
14 1 2 5 mulgnn0dir G Mnd m 0 n 0 A B m + n · ˙ A = m · ˙ A + ˙ n · ˙ A
15 10 11 12 13 14 syl13anc G Mnd A B X C Y C m 0 n 0 m + n · ˙ A = m · ˙ A + ˙ n · ˙ A
16 15 ralrimivva G Mnd A B X C Y C m 0 n 0 m + n · ˙ A = m · ˙ A + ˙ n · ˙ A
17 simprl G Mnd A B X C Y C X C
18 simprr G Mnd A B X C Y C Y C
19 nn0sscn 0
20 19 a1i G Mnd A B X C Y C 0
21 9 16 17 18 20 cyccom G Mnd A B X C Y C X + ˙ Y = Y + ˙ X