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

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 
|- .x. = ( .g ` G )
cycsubmcmn.f 
|- F = ( x e. NN0 |-> ( x .x. A ) )
cycsubmcmn.c 
|- C = ran F
Assertion cycsubmcmn 
|- ( ( G e. Mnd /\ A e. B ) -> ( G |`s C ) e. CMnd )

Proof

Step Hyp Ref Expression
1 cycsubmcmn.b 
 |-  B = ( Base ` G )
2 cycsubmcmn.t 
 |-  .x. = ( .g ` G )
3 cycsubmcmn.f 
 |-  F = ( x e. NN0 |-> ( x .x. A ) )
4 cycsubmcmn.c 
 |-  C = ran F
5 1 2 3 4 cycsubm 
 |-  ( ( G e. Mnd /\ A e. B ) -> C e. ( SubMnd ` G ) )
6 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
7 eqid 
 |-  ( G |`s C ) = ( G |`s C )
8 1 6 7 issubm2 
 |-  ( G e. Mnd -> ( C e. ( SubMnd ` G ) <-> ( C C_ B /\ ( 0g ` G ) e. C /\ ( G |`s C ) e. Mnd ) ) )
9 8 adantr 
 |-  ( ( G e. Mnd /\ A e. B ) -> ( C e. ( SubMnd ` G ) <-> ( C C_ B /\ ( 0g ` G ) e. C /\ ( G |`s C ) e. Mnd ) ) )
10 simp3 
 |-  ( ( C C_ B /\ ( 0g ` G ) e. C /\ ( G |`s C ) e. Mnd ) -> ( G |`s C ) e. Mnd )
11 9 10 biimtrdi 
 |-  ( ( G e. Mnd /\ A e. B ) -> ( C e. ( SubMnd ` G ) -> ( G |`s C ) e. Mnd ) )
12 5 11 mpd 
 |-  ( ( G e. Mnd /\ A e. B ) -> ( G |`s C ) e. Mnd )
13 7 submbas 
 |-  ( C e. ( SubMnd ` G ) -> C = ( Base ` ( G |`s C ) ) )
14 5 13 syl 
 |-  ( ( G e. Mnd /\ A e. B ) -> C = ( Base ` ( G |`s C ) ) )
15 14 eqcomd 
 |-  ( ( G e. Mnd /\ A e. B ) -> ( Base ` ( G |`s C ) ) = C )
16 15 eleq2d 
 |-  ( ( G e. Mnd /\ A e. B ) -> ( x e. ( Base ` ( G |`s C ) ) <-> x e. C ) )
17 15 eleq2d 
 |-  ( ( G e. Mnd /\ A e. B ) -> ( y e. ( Base ` ( G |`s C ) ) <-> y e. C ) )
18 16 17 anbi12d 
 |-  ( ( G e. Mnd /\ A e. B ) -> ( ( x e. ( Base ` ( G |`s C ) ) /\ y e. ( Base ` ( G |`s C ) ) ) <-> ( x e. C /\ y e. C ) ) )
19 eqid 
 |-  ( +g ` G ) = ( +g ` G )
20 1 2 3 4 19 cycsubmcom 
 |-  ( ( ( G e. Mnd /\ A e. B ) /\ ( x e. C /\ y e. C ) ) -> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) )
21 5 adantr 
 |-  ( ( ( G e. Mnd /\ A e. B ) /\ ( x e. C /\ y e. C ) ) -> C e. ( SubMnd ` G ) )
22 7 19 ressplusg 
 |-  ( C e. ( SubMnd ` G ) -> ( +g ` G ) = ( +g ` ( G |`s C ) ) )
23 22 eqcomd 
 |-  ( C e. ( SubMnd ` G ) -> ( +g ` ( G |`s C ) ) = ( +g ` G ) )
24 23 oveqd 
 |-  ( C e. ( SubMnd ` G ) -> ( x ( +g ` ( G |`s C ) ) y ) = ( x ( +g ` G ) y ) )
25 23 oveqd 
 |-  ( C e. ( SubMnd ` G ) -> ( y ( +g ` ( G |`s C ) ) x ) = ( y ( +g ` G ) x ) )
26 24 25 eqeq12d 
 |-  ( C e. ( SubMnd ` G ) -> ( ( x ( +g ` ( G |`s C ) ) y ) = ( y ( +g ` ( G |`s C ) ) x ) <-> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) )
27 21 26 syl 
 |-  ( ( ( G e. Mnd /\ A e. B ) /\ ( x e. C /\ y e. C ) ) -> ( ( x ( +g ` ( G |`s C ) ) y ) = ( y ( +g ` ( G |`s C ) ) x ) <-> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) )
28 20 27 mpbird 
 |-  ( ( ( G e. Mnd /\ A e. B ) /\ ( x e. C /\ y e. C ) ) -> ( x ( +g ` ( G |`s C ) ) y ) = ( y ( +g ` ( G |`s C ) ) x ) )
29 28 ex 
 |-  ( ( G e. Mnd /\ A e. B ) -> ( ( x e. C /\ y e. C ) -> ( x ( +g ` ( G |`s C ) ) y ) = ( y ( +g ` ( G |`s C ) ) x ) ) )
30 18 29 sylbid 
 |-  ( ( G e. Mnd /\ A e. B ) -> ( ( x e. ( Base ` ( G |`s C ) ) /\ y e. ( Base ` ( G |`s C ) ) ) -> ( x ( +g ` ( G |`s C ) ) y ) = ( y ( +g ` ( G |`s C ) ) x ) ) )
31 30 ralrimivv 
 |-  ( ( G e. Mnd /\ A e. B ) -> A. x e. ( Base ` ( G |`s C ) ) A. y e. ( Base ` ( G |`s C ) ) ( x ( +g ` ( G |`s C ) ) y ) = ( y ( +g ` ( G |`s C ) ) x ) )
32 eqid 
 |-  ( Base ` ( G |`s C ) ) = ( Base ` ( G |`s C ) )
33 eqid 
 |-  ( +g ` ( G |`s C ) ) = ( +g ` ( G |`s C ) )
34 32 33 iscmn 
 |-  ( ( G |`s C ) e. CMnd <-> ( ( G |`s C ) e. Mnd /\ A. x e. ( Base ` ( G |`s C ) ) A. y e. ( Base ` ( G |`s C ) ) ( x ( +g ` ( G |`s C ) ) y ) = ( y ( +g ` ( G |`s C ) ) x ) ) )
35 12 31 34 sylanbrc 
 |-  ( ( G e. Mnd /\ A e. B ) -> ( G |`s C ) e. CMnd )