This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )