Metamath Proof Explorer

Theorem cntrcmnd

Description: The center of a monoid is a commutative submonoid. (Contributed by Thierry Arnoux, 21-Aug-2023)

Ref Expression
Hypothesis cntrcmnd.z 
|- Z = ( M |`s ( Cntr ` M ) )
Assertion cntrcmnd 
|- ( M e. Mnd -> Z e. CMnd )

Proof

Step Hyp Ref Expression
1 cntrcmnd.z 
 |-  Z = ( M |`s ( Cntr ` M ) )
2 eqid 
 |-  ( Base ` M ) = ( Base ` M )
3 2 cntrss 
 |-  ( Cntr ` M ) C_ ( Base ` M )
4 1 2 ressbas2 
 |-  ( ( Cntr ` M ) C_ ( Base ` M ) -> ( Cntr ` M ) = ( Base ` Z ) )
5 3 4 mp1i 
 |-  ( M e. Mnd -> ( Cntr ` M ) = ( Base ` Z ) )
6 fvex 
 |-  ( Cntr ` M ) e. _V
7 eqid 
 |-  ( +g ` M ) = ( +g ` M )
8 1 7 ressplusg 
 |-  ( ( Cntr ` M ) e. _V -> ( +g ` M ) = ( +g ` Z ) )
9 6 8 mp1i 
 |-  ( M e. Mnd -> ( +g ` M ) = ( +g ` Z ) )
10 eqid 
 |-  ( Cntz ` M ) = ( Cntz ` M )
11 2 10 cntrval 
 |-  ( ( Cntz ` M ) ` ( Base ` M ) ) = ( Cntr ` M )
12 ssid 
 |-  ( Base ` M ) C_ ( Base ` M )
13 2 10 cntzsubm 
 |-  ( ( M e. Mnd /\ ( Base ` M ) C_ ( Base ` M ) ) -> ( ( Cntz ` M ) ` ( Base ` M ) ) e. ( SubMnd ` M ) )
14 12 13 mpan2 
 |-  ( M e. Mnd -> ( ( Cntz ` M ) ` ( Base ` M ) ) e. ( SubMnd ` M ) )
15 11 14 eqeltrrid 
 |-  ( M e. Mnd -> ( Cntr ` M ) e. ( SubMnd ` M ) )
16 1 submmnd 
 |-  ( ( Cntr ` M ) e. ( SubMnd ` M ) -> Z e. Mnd )
17 15 16 syl 
 |-  ( M e. Mnd -> Z e. Mnd )
18 simp2 
 |-  ( ( M e. Mnd /\ x e. ( Cntr ` M ) /\ y e. ( Cntr ` M ) ) -> x e. ( Cntr ` M ) )
19 simp3 
 |-  ( ( M e. Mnd /\ x e. ( Cntr ` M ) /\ y e. ( Cntr ` M ) ) -> y e. ( Cntr ` M ) )
20 3 19 sseldi 
 |-  ( ( M e. Mnd /\ x e. ( Cntr ` M ) /\ y e. ( Cntr ` M ) ) -> y e. ( Base ` M ) )
21 eqid 
 |-  ( Cntr ` M ) = ( Cntr ` M )
22 2 7 21 cntri 
 |-  ( ( x e. ( Cntr ` M ) /\ y e. ( Base ` M ) ) -> ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) )
23 18 20 22 syl2anc 
 |-  ( ( M e. Mnd /\ x e. ( Cntr ` M ) /\ y e. ( Cntr ` M ) ) -> ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) )
24 5 9 17 23 iscmnd 
 |-  ( M e. Mnd -> Z e. CMnd )