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