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 ↾ 𝑠 Cntr ⁡ M
Assertion cntrabl ⊢ M ∈ Grp → Z ∈ Abel

Proof

Step Hyp Ref Expression
1 cntrcmnd.z ⊢ Z = M ↾ 𝑠 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 ⊆ Base M
6 2 3 cntzsubg ⊢ M ∈ Grp ∧ Base M ⊆ Base M → Cntz ⁡ M ⁡ Base M ∈ SubGrp ⁡ M
7 5 6 mpan2 ⊢ M ∈ Grp → Cntz ⁡ M ⁡ Base M ∈ SubGrp ⁡ M
8 4 7 eqeltrrid ⊢ M ∈ Grp → Cntr ⁡ M ∈ SubGrp ⁡ M
9 1 subggrp ⊢ Cntr ⁡ M ∈ SubGrp ⁡ M → Z ∈ Grp
10 8 9 syl ⊢ M ∈ Grp → Z ∈ Grp
11 grpmnd ⊢ M ∈ Grp → M ∈ Mnd
12 1 cntrcmnd ⊢ M ∈ Mnd → Z ∈ CMnd
13 11 12 syl ⊢ M ∈ Grp → Z ∈ CMnd
14 isabl ⊢ Z ∈ Abel ↔ Z ∈ Grp ∧ Z ∈ CMnd
15 10 13 14 sylanbrc ⊢ M ∈ Grp → Z ∈ Abel