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 \in Grp \to Z \in Abel$

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} \subseteq {Base}_{M}$
6	2 3	cntzsubg	$⊢ (M \in Grp \land {Base}_{M} \subseteq {Base}_{M}) \to Cntz (M) ({Base}_{M}) \in SubGrp (M)$
7	5 6	mpan2	$⊢ M \in Grp \to Cntz (M) ({Base}_{M}) \in SubGrp (M)$
8	4 7	eqeltrrid	$⊢ M \in Grp \to Cntr (M) \in SubGrp (M)$
9	1	subggrp	$⊢ Cntr (M) \in SubGrp (M) \to Z \in Grp$
10	8 9	syl	$⊢ M \in Grp \to Z \in Grp$
11		grpmnd	$⊢ M \in Grp \to M \in Mnd$
12	1	cntrcmnd	$⊢ M \in Mnd \to Z \in CMnd$
13	11 12	syl	$⊢ M \in Grp \to Z \in CMnd$
14		isabl	$⊢ Z \in Abel \leftrightarrow (Z \in Grp \land Z \in CMnd)$
15	10 13 14	sylanbrc	$⊢ M \in Grp \to Z \in Abel$

Metamath Proof Explorer