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 𝑍 = ( 𝑀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 )