Theorem cntrabl

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

	Ref	Expression
Hypothesis	cntrcmnd.z	⊢ 𝑍 = ( 𝑀 ↾s ( Cntr ‘ 𝑀 ) )
Assertion	cntrabl	⊢ ( 𝑀 ∈ Grp → 𝑍 ∈ Abel )

Proof

Step	Hyp	Ref	Expression
1		cntrcmnd.z	⊢ 𝑍 = ( 𝑀 ↾s ( Cntr ‘ 𝑀 ) )
2		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
3		eqid	⊢ ( Cntz ‘ 𝑀 ) = ( Cntz ‘ 𝑀 )
4	2 3	cntrval	⊢ ( ( Cntz ‘ 𝑀 ) ‘ ( Base ‘ 𝑀 ) ) = ( Cntr ‘ 𝑀 )
5		ssid	⊢ ( Base ‘ 𝑀 ) ⊆ ( Base ‘ 𝑀 )
6	2 3	cntzsubg	⊢ ( ( 𝑀 ∈ Grp ∧ ( Base ‘ 𝑀 ) ⊆ ( Base ‘ 𝑀 ) ) → ( ( Cntz ‘ 𝑀 ) ‘ ( Base ‘ 𝑀 ) ) ∈ ( SubGrp ‘ 𝑀 ) )
7	5 6	mpan2	⊢ ( 𝑀 ∈ Grp → ( ( Cntz ‘ 𝑀 ) ‘ ( Base ‘ 𝑀 ) ) ∈ ( SubGrp ‘ 𝑀 ) )
8	4 7	eqeltrrid	⊢ ( 𝑀 ∈ Grp → ( Cntr ‘ 𝑀 ) ∈ ( SubGrp ‘ 𝑀 ) )
9	1	subggrp	⊢ ( ( Cntr ‘ 𝑀 ) ∈ ( SubGrp ‘ 𝑀 ) → 𝑍 ∈ Grp )
10	8 9	syl	⊢ ( 𝑀 ∈ Grp → 𝑍 ∈ Grp )
11		grpmnd	⊢ ( 𝑀 ∈ Grp → 𝑀 ∈ Mnd )
12	1	cntrcmnd	⊢ ( 𝑀 ∈ Mnd → 𝑍 ∈ CMnd )
13	11 12	syl	⊢ ( 𝑀 ∈ Grp → 𝑍 ∈ CMnd )
14		isabl	⊢ ( 𝑍 ∈ Abel ↔ ( 𝑍 ∈ Grp ∧ 𝑍 ∈ CMnd ) )
15	10 13 14	sylanbrc	⊢ ( 𝑀 ∈ Grp → 𝑍 ∈ Abel )