Metamath Proof Explorer

Theorem cmnbascntr

Description: The base set of a commutative monoid is its center. (Contributed by SN, 21-Mar-2025)

Ref Expression
Hypotheses cmnbascntr.b 
|- B = ( Base ` G )
cmnbascntr.z 
|- Z = ( Cntr ` G )
Assertion cmnbascntr 
|- ( G e. CMnd -> B = Z )

Proof

Step Hyp Ref Expression
1 cmnbascntr.b 
 |-  B = ( Base ` G )
2 cmnbascntr.z 
 |-  Z = ( Cntr ` G )
3 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
4 1 3 cntrval 
 |-  ( ( Cntz ` G ) ` B ) = ( Cntr ` G )
5 ssid 
 |-  B C_ B
6 eqid 
 |-  ( +g ` G ) = ( +g ` G )
7 1 6 3 cntzval 
 |-  ( B C_ B -> ( ( Cntz ` G ) ` B ) = { x e. B | A. y e. B ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) } )
8 5 7 ax-mp 
 |-  ( ( Cntz ` G ) ` B ) = { x e. B | A. y e. B ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) }
9 2 4 8 3eqtr2i 
 |-  Z = { x e. B | A. y e. B ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) }
10 1 6 cmncom 
 |-  ( ( G e. CMnd /\ x e. B /\ y e. B ) -> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) )
11 10 3expa 
 |-  ( ( ( G e. CMnd /\ x e. B ) /\ y e. B ) -> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) )
12 11 ralrimiva 
 |-  ( ( G e. CMnd /\ x e. B ) -> A. y e. B ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) )
13 12 rabeqcda 
 |-  ( G e. CMnd -> { x e. B | A. y e. B ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) } = B )
14 9 13 eqtr2id 
 |-  ( G e. CMnd -> B = Z )