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

Metamath Proof Explorer

Theorem cntrabl

Description: The center of a group is an abelian group. (Contributed by Thierry Arnoux, 21-Aug-2023)

Ref Expression
Hypothesis cntrcmnd.z 
|- Z = ( M |`s ( Cntr ` M ) )
Assertion cntrabl 
|- ( M e. Grp -> Z e. Abel )

Proof

Step Hyp Ref Expression
1 cntrcmnd.z 
 |-  Z = ( M |`s ( Cntr ` M ) )
2 eqid 
 |-  ( Base ` M ) = ( Base ` M )
3 eqid 
 |-  ( Cntz ` M ) = ( Cntz ` M )
4 2 3 cntrval 
 |-  ( ( Cntz ` M ) ` ( Base ` M ) ) = ( Cntr ` M )
5 ssid 
 |-  ( Base ` M ) C_ ( Base ` M )
6 2 3 cntzsubg 
 |-  ( ( M e. Grp /\ ( Base ` M ) C_ ( Base ` M ) ) -> ( ( Cntz ` M ) ` ( Base ` M ) ) e. ( SubGrp ` M ) )
7 5 6 mpan2 
 |-  ( M e. Grp -> ( ( Cntz ` M ) ` ( Base ` M ) ) e. ( SubGrp ` M ) )
8 4 7 eqeltrrid 
 |-  ( M e. Grp -> ( Cntr ` M ) e. ( SubGrp ` M ) )
9 1 subggrp 
 |-  ( ( Cntr ` M ) e. ( SubGrp ` M ) -> Z e. Grp )
10 8 9 syl 
 |-  ( M e. Grp -> Z e. Grp )
11 grpmnd 
 |-  ( M e. Grp -> M e. Mnd )
12 1 cntrcmnd 
 |-  ( M e. Mnd -> Z e. CMnd )
13 11 12 syl 
 |-  ( M e. Grp -> Z e. CMnd )
14 isabl 
 |-  ( Z e. Abel <-> ( Z e. Grp /\ Z e. CMnd ) )
15 10 13 14 sylanbrc 
 |-  ( M e. Grp -> Z e. Abel )