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 )