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
|- .x. = ( .g ` G )
cycsubmcom.f
|- F = ( x e. NN0 |-> ( x .x. A ) )
cycsubmcom.c
|- C = ran F
cycsubmcom.p
|- .+ = ( +g ` G )
Assertion cycsubmcom
|- ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) -> ( X .+ Y ) = ( Y .+ X ) )

Proof

Step Hyp Ref Expression
1 cycsubmcom.b
 |-  B = ( Base ` G )
2 cycsubmcom.t
 |-  .x. = ( .g ` G )
3 cycsubmcom.f
 |-  F = ( x e. NN0 |-> ( x .x. A ) )
4 cycsubmcom.c
 |-  C = ran F
5 cycsubmcom.p
 |-  .+ = ( +g ` G )
6 1 2 3 4 cycsubmel
 |-  ( c e. C <-> E. i e. NN0 c = ( i .x. A ) )
7 6 biimpi
 |-  ( c e. C -> E. i e. NN0 c = ( i .x. A ) )
8 7 adantl
 |-  ( ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) /\ c e. C ) -> E. i e. NN0 c = ( i .x. A ) )
9 8 ralrimiva
 |-  ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) -> A. c e. C E. i e. NN0 c = ( i .x. A ) )
10 simplll
 |-  ( ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) /\ ( m e. NN0 /\ n e. NN0 ) ) -> G e. Mnd )
11 simprl
 |-  ( ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) /\ ( m e. NN0 /\ n e. NN0 ) ) -> m e. NN0 )
12 simprr
 |-  ( ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) /\ ( m e. NN0 /\ n e. NN0 ) ) -> n e. NN0 )
13 simpllr
 |-  ( ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) /\ ( m e. NN0 /\ n e. NN0 ) ) -> A e. B )
14 1 2 5 mulgnn0dir
 |-  ( ( G e. Mnd /\ ( m e. NN0 /\ n e. NN0 /\ A e. B ) ) -> ( ( m + n ) .x. A ) = ( ( m .x. A ) .+ ( n .x. A ) ) )
15 10 11 12 13 14 syl13anc
 |-  ( ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) /\ ( m e. NN0 /\ n e. NN0 ) ) -> ( ( m + n ) .x. A ) = ( ( m .x. A ) .+ ( n .x. A ) ) )
16 15 ralrimivva
 |-  ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) -> A. m e. NN0 A. n e. NN0 ( ( m + n ) .x. A ) = ( ( m .x. A ) .+ ( n .x. A ) ) )
17 simprl
 |-  ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) -> X e. C )
18 simprr
 |-  ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) -> Y e. C )
19 nn0sscn
 |-  NN0 C_ CC
20 19 a1i
 |-  ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) -> NN0 C_ CC )
21 9 16 17 18 20 cyccom
 |-  ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) -> ( X .+ Y ) = ( Y .+ X ) )